TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Poisson modification is subharmonic and majorizes the original function

Statement

Let $u$ be subharmonic on a complex domain $Ω$ and let $D ⋐ Ω$ be an open disc. Then the Poisson modification $P_{D} u$ of Poisson modification on a compactly contained disc is well defined, subharmonic on $Ω$ , harmonic on $D$ , and satisfies $P_{D} u \geq u$ on $Ω$ .

Facts & Assumptions

Given: A subharmonic function $u$ on a complex domain $Ω$ and an open disc $D ⋐ Ω$ .

[L1]

A boundary approximation for $u ∣_{\partial D}$ produces harmonic functions $h_{n}$ on $D$ with continuous boundary values $ϕ_{n}$ that decrease pointwise on $\partial D$ (Poisson modification on a compactly contained disc, The Poisson integral gives the unique continuous harmonic extension on the closed unit disc, Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate).

[L2]

If a harmonic function dominates a subharmonic function on the boundary of a compactly contained disc, then it dominates it throughout the disc (Subharmonicity is equivalent to harmonic comparison on compactly contained discs).

[L3]

Subharmonic pieces glue when the inside boundary limsup is dominated by the outside value (Subharmonic pieces glue across a boundary under the limsup inequality).

[L4]

An increasing harmonic sequence that is bounded above at one point converges locally uniformly to a harmonic limit (An increasing harmonic sequence converges locally uniformly to a harmonic limit or diverges to +infinity).

[L5]

A subharmonic function is locally integrable, so it is finite almost everywhere on every disc in its domain (Plane subharmonic functions are locally integrable).

Proof

technique · direct

1.1

Choose a boundary approximation $(ϕ_{n})$ for $u ∣_{\partial D}$ , and let $h_{n}$ be the associated harmonic functions from [L1]. Because $ϕ_{n} \geq u$ on $\partial D$ , [L2] gives $h_{n} \geq u$ on $D$ for every $n$ . The sequence $(h_{n})$ is decreasing because the boundary data are decreasing.

L1L2givenchoose

2.1

Let $M$ be an upper bound for $ϕ_{1}$ on $\partial D$ . Then each $M - h_{n}$ is a nonnegative harmonic function on $D$ , and the sequence $(M - h_{n})$ is increasing. By [L5], choose $z_{0} \in D$ with $u (z_{0}) > - \infty$ . Step 1.1 gives $0 \leq M - h_{n} (z_{0}) \leq M - u (z_{0})$ , so [L4] applied to $(M - h_{n})$ yields a harmonic limit $H$ on $D$ . Consequently $h : = M - H = \inf_{n} h_{n}$ is harmonic on $D$ .

step 1.1L4L5choose

3.1

The inside function $h$ is independent of the chosen boundary approximation. Indeed, if $k$ is obtained from another approximation $(ψ_{m})$ , then $h$ is harmonic on $D$ and its boundary limsup satisfies [step 1.1, step 2.1, L2] ${lim sup}_{\begin{array}{c} z \to ζ \\ z \in D \end{array}} h (z) \leq ϕ_{n} (ζ) (ζ \in \partial D)$ for every fixed $n$ , hence $lim sup h \leq u \leq ψ_{m}$ on the boundary. Applying [L2] to the harmonic function $k_{m}$ extending $ψ_{m}$ gives $h \leq k_{m}$ on $D$ for every $m$ , so $h \leq k$ . Symmetry gives $k \leq h$ .

step 1.1step 2.1L2

4.1

By step 1.1, $h \geq u$ on $D$ , and by step 3.1 this harmonic function is intrinsic. Moreover, for every $ζ \in \partial D$ and every fixed $n$ , one has $h \leq h_{n}$ on $D$ and $h_{n} (ζ) = ϕ_{n} (ζ)$ , so [step 1.1, step 2.1] ${lim sup}_{\begin{array}{c} z \to ζ \\ z \in D \end{array}} h (z) \leq ϕ_{n} (ζ) .$ Letting $n \to \infty$ yields ${lim sup}_{z \to ζ, z \in D} h (z) \leq u (ζ)$ .

step 1.1step 2.1

5.1

The Poisson modification equals $h$ on $D$ and $u$ on $Ω ∖ D$ . Step 4.1 provides the seam inequality, so [L3] shows that $P_{D} u$ is subharmonic on $Ω$ . It is harmonic on $D$ by step 2.1, equals $u$ outside $D$ by definition, and majorizes $u$ on $D$ by step 4.1. Hence $P_{D} u \geq u$ on all of $Ω$ .

L3step 2.1step 4.1∎

Depends on

Used by

Cited to discharge well-definedness by Poisson modification on a compactly contained disc.

Dependency tree · two levels

25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Sheldon Axler, Paul Bourdon, and Wade Ramey, Harmonic Function Theory, 2nd ed. (standard reference, not scraped)