Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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 PDu of Poisson modification on a compactly contained disc is well defined, subharmonic on Ω, harmonic on D, and satisfies PDu≥u on Ω.

Facts & Assumptions

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

[L1]

A boundary approximation for u∣∂D produces harmonic functions hn on D with continuous boundary values ϕn that decrease pointwise on ∂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.1L1L2givenchoose

Choose a boundary approximation (ϕn) for u∣∂D, and let hn be the associated harmonic functions from [L1]. Because ϕn≥u on ∂D, [L2] gives hn≥u on D for every n. The sequence (hn) is decreasing because the boundary data are decreasing.

2.1step 1.1L4L5choose

Let M be an upper bound for ϕ1 on ∂D. Then each M−hn is a nonnegative harmonic function on D, and the sequence (M−hn) is increasing. By [L5], choose z0∈D with u(z0)>−∞. Step 1.1 gives 0≤M−hn(z0)≤M−u(z0), so [L4] applied to (M−hn) yields a harmonic limit H on D. Consequently h:=M−H=inf⁡nhn is harmonic on D.

3.1step 1.1step 2.1L2

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⁡z→ζz∈Dh(z)≤ϕn(ζ)(ζ∈∂D) for every fixed n, hence lim sup⁡h≤u≤ψm on the boundary. Applying [L2] to the harmonic function km extending ψm gives h≤km on D for every m, so h≤k. Symmetry gives k≤h.

4.1step 1.1step 2.1

By step 1.1, h≥u on D, and by step 3.1 this harmonic function is intrinsic. Moreover, for every ζ∈∂D and every fixed n, one has h≤hn on D and hn(ζ)=ϕn(ζ), so [step 1.1, step 2.1] lim sup⁡z→ζz∈Dh(z)≤ϕn(ζ). Letting n→∞ yields lim sup⁡z→ζ, z∈Dh(z)≤u(ζ).

5.1L3step 2.1step 4.1∎

The Poisson modification equals h on D and u on Ω∖D. Step 4.1 provides the seam inequality, so [L3] shows that PDu 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 PDu≥u on all of Ω.

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