Alphabeta Math
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.

✓ 23 results · all verified · 8 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 15 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Subharmonic Functions and the Dirichlet Problem

1 · Prerequisites

2 · Summary

This page fixes the standard extended-real, upper-semicontinuous convention for plane subharmonicity, proves the comparison, C2, local-integrability, and stability theorems that make the class workable, and then develops Perron's construction for the bounded plane Dirichlet problem. The second half turns barriers into boundary regularity criteria, proves the exterior-disc and exterior-cone tests, records the complementary-component and boundary-component routes to regularity, and finishes with conformal transport of continuous Dirichlet solutions across closure-homeomorphic biholomorphisms.

3 · Logical flowchart

4 · Definitions, theorems and proofs

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

This page uses the standard upper-semicontinuous subharmonic convention

The subharmonic functions on this page take values in [−∞,∞), are required to be upper semicontinuous, and are excluded from being identically −∞ on any connected component of the domain. This is the standard potential-theoretic convention used by the sources behind the page, and it is the one compatible with log⁡∣f∣ for a holomorphic function and with Perron's method for the Dirichlet problem.

The older convention that a subharmonic function is merely a continuous real-valued function satisfying the submean inequality is recovered as the special case where the function never takes the value −∞ and happens to be continuous. The harmonic comparison theorems on the page are written so that the harmonic notion from Plane harmonic functions remains the same while the subharmonic class is large enough to include logarithmic singularities.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Subharmonic functions on plane domains

Definition

Let Ω⊆C be a complex domain. A function u:Ω→[−∞,∞) is subharmonic on Ω when:

  1. u is upper semicontinuous;
  2. on no connected component of Ω is u identically −∞;
  3. for every closed disc D(a,r)‾⊆Ω, u(a)≤12π∫02πu(a+reit) dt, where the integral is taken in the extended-real sense.

Remarks

The radius r is always positive. The value u(a) is allowed to be −∞, in which case the submean inequality is automatic.

On a circle, upper semicontinuity gives a finite upper bound, so the integral above can only fail in the downward direction; the next lemma records that the boundary function is Borel and that the average is therefore defined in [−∞,∞).

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Superharmonic functions on plane domains

Definition

Let Ω⊆C be a complex domain. A function v:Ω→(−∞,∞] is superharmonic on Ω when −v is subharmonic on Ω in the sense of Subharmonic functions on plane domains.

Remarks

Thus a superharmonic function is lower semicontinuous, may take the value +∞, and is excluded from being identically +∞ on a connected component.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Upper semicontinuous functions are Borel and their circle averages are defined

Statement

Let Ω⊆C be open and let u:Ω→[−∞,∞) be upper semicontinuous. Then:

  1. u is Borel measurable;
  2. for every circle C={a+reit:0≤t≤2π}⊆Ω, the boundary function t↦u(a+reit) is Borel measurable and bounded above, so its average 12π∫02πu(a+reit) dt is a well-defined element of [−∞,∞).

Facts & Assumptions

Given: An upper semicontinuous function u:Ω→[−∞,∞) and a circle C={a+reit:0≤t≤2π}⊆Ω.

[A1]

The function u is upper semicontinuous on Ω, and the circle C lies in Ω.

Proof

technique · direct
1.1A1

For every real α, the set {z∈Ω:u(z)<α} is open because u is upper semicontinuous. Hence the sets {u≥α} are closed, and therefore u is Borel measurable.

1.2A1

The circle C is compact. If u is not identically −∞ on C, upper semicontinuity gives a point of maximum and therefore a finite upper bound M on C; if u≡−∞ on C, then −∞ is already an upper bound. So the boundary function on [0,2π] is Borel measurable and bounded above.

2.1step 1.1

The parametrization t↦a+reit is continuous, so composing it with the Borel function from step 1.1 makes t↦u(a+reit) Borel measurable on [0,2π].

3.1step 2.1step 1.2∎

A Borel measurable function bounded above on a finite interval has an extended-real integral in [−∞,∞), so the displayed circle average is well defined.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

Subharmonicity is equivalent to harmonic comparison on compactly contained discs

Statement

Let Ω⊆C be a complex domain and let u:Ω→[−∞,∞). The following are equivalent.

  1. u is subharmonic on Ω.
  2. u is upper semicontinuous, is not identically −∞ on any connected component, and for every closed disc D(a,r)‾⊆Ω and every function h continuous on D(a,r)‾, harmonic on D(a,r), and satisfying h≥u on ∂D(a,r), one has h≥u on D(a,r).

Facts & Assumptions

Given: A complex domain Ω, a function u:Ω→[−∞,∞), and a closed disc D(a,r)‾⊆Ω.

[L1]

Subharmonic means upper semicontinuous, not identically −∞ on a connected component, and satisfying the circle submean inequality on every closed disc in the domain (Subharmonic functions on plane domains).

[L2]

For an upper semicontinuous extended-real function, circle boundary values are Borel measurable and bounded above, so decreasing continuous approximants to the boundary data have well-defined circle averages (Upper semicontinuous functions are Borel and their circle averages are defined).

[L3]

Continuous boundary data on the unit circle have a unique continuous harmonic Poisson extension to the closed disc (The Poisson integral on the unit disc, The Poisson integral gives the unique continuous harmonic extension on the closed unit disc).

[L4]

Plane harmonic functions satisfy the circle mean-value property, and affine holomorphic changes of coordinate preserve harmonicity, so the unit-disc Poisson solution transports to every Euclidean disc (Plane harmonic functions satisfy the mean-value property, Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate).

[L5]

Monotone convergence for the nonnegative integral identifies the limit of the circle integrals of the increasing nonnegative boundary functions M−ϕn with the integral of their pointwise limit M−g (Monotone convergence for the integral).

[L6]

A subharmonic function that attains a finite interior maximum is constant on its connected component (A plane subharmonic function with an interior maximum is constant on its component).

Proof

technique · direct
1.1L1L4L6given

Assume condition 1. Let h be continuous on D(a,r)‾, harmonic on D(a,r), and satisfy h≥u on ∂D(a,r). On D(a,r) define v:=u−h. For z∈D(a,r) and every 0<ρ<dist⁡(z,∂D(a,r)), the submean inequality for u and the circle mean-value property for h give [L1, L4, given] v(z)=u(z)−h(z)≤12π∫02π(u(z+ρeit)−h(z+ρeit)) dt. Thus v is subharmonic on D(a,r). If some point of D(a,r) satisfied v>0, then upper semicontinuity on the compact disc would make v attain a positive interior maximum there, contradicting [L6] because v≤0 on ∂D(a,r). Hence v≤0 on D(a,r), so h≥u throughout the disc. This is condition 2.

1.2givenL2construct

Assume condition 2. Fix a closed disc D(a,r)‾⊆Ω and write g(ζ)=u(ζ) on ∂D(a,r). By [L2], g is Borel measurable and bounded above. On the compact circle, define [given, L2, construct] ϕn(ζ):=sup⁡η∈∂D(a,r)(g(η)−n∣ζ−η∣). Each ϕn is finite and continuous, satisfies ϕn≥g, and decreases pointwise to g because g is upper semicontinuous.

2.1step 1.2L3L4

Transporting the Poisson solution from the unit disc by [L3] and [L4], let hn be the harmonic function on D(a,r), continuous on D(a,r)‾, whose boundary values are ϕn. Since ϕn≥g=u on ∂D(a,r), condition 2 gives u≤hn on D(a,r). Evaluating at the center and using the Poisson formula at the center of a disc, [step 1.2, L3, L4] u(a)≤hn(a)=12π∫02πϕn(a+reit) dt.

3.1step 1.2step 2.1L1L5∎

Let M be an upper bound for ϕ1 on the circle. Then M−ϕn is an increasing sequence of nonnegative boundary functions, so [L5] gives [step 1.2, step 2.1, L1, L5] lim⁡n→∞12π∫02πϕn(a+reit) dt=12π∫02πu(a+reit) dt. Passing to the limit in step 2.1 yields the circle submean inequality at a. Since the disc was arbitrary and upper semicontinuity is already part of condition 2, condition 1 follows.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

A C^2 function is subharmonic exactly when its Laplacian is nonnegative

Statement

Let Ω⊆C be open and let u∈C2(Ω,R). Then u is subharmonic on Ω if and only if Δu=uxx+uyy≥0 throughout Ω.

Facts & Assumptions

Given: An open set Ω⊆C and a function u∈C2(Ω,R).

[L1]

Subharmonicity on a domain is equivalent to harmonic comparison on every compactly contained disc (Subharmonicity is equivalent to harmonic comparison on compactly contained discs).

Proof

technique · direct
1.1L1givenalgebra

Assume first that u is subharmonic. Fix a∈Ω and choose r>0 with D(a,r)‾⊆Ω. For 0<ρ<r, Taylor's formula in the direction eit gives [L1, given, algebra] u(a+ρeit)=u(a)+ρ ∇u(a) ⁣⋅ ⁣eit+ρ22 eit ⁣T(D2u(a))eit+o(ρ2). Averaging over t kills the linear term and averages the quadratic term to ρ24Δu(a), so the submean inequality yields 0≤12π∫02πu(a+ρeit) dt−u(a)=ρ24Δu(a)+o(ρ2). Dividing by ρ2 and letting ρ↓0 gives Δu(a)≥0.

2.1L1algebra∎

Assume now that Δu≥0 on Ω. Fix a closed disc D(a,r)‾⊆Ω, and let h be continuous on D(a,r)‾, harmonic on D(a,r), and satisfy h≥u on ∂D(a,r). Put w=u−h. Then w is continuous on D(a,r)‾, belongs to C2(D(a,r)), satisfies Δw=Δu≥0 on D(a,r), and has w≤0 on ∂D(a,r). If some point p∈D(a,r) had w(p)>0, choose 0<ε<w(p)/r2 and define wε(z):=w(z)+ε∣z−a∣2. On the boundary one has wε≤εr2<w(p)≤wε(p), so wε attains its maximum at an interior point q∈D(a,r). The second-derivative test there gives Δwε(q)≤0, but Δwε=Δw+4ε≥4ε>0, a contradiction. Therefore w≤0 on D(a,r), so u≤h on the whole disc. Since the disc and the harmonic boundary majorant h were arbitrary, [L1] shows that u is subharmonic on Ω.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

Plane subharmonic functions are locally integrable

Statement

Every subharmonic function on a complex domain belongs to Lloc1.

Facts & Assumptions

Given: A subharmonic function u on a complex domain Ω.

[L1]

On every closed disc inside the domain, a harmonic function that dominates u on the boundary dominates u throughout the disc (Subharmonicity is equivalent to harmonic comparison on compactly contained discs).

[L2]

On a compact circle, the boundary values of an upper semicontinuous function are Borel measurable and bounded above, so the circle averages in the submean inequality are finite or −∞ (Upper semicontinuous functions are Borel and their circle averages are defined).

[L4]

For a nonnegative Borel function F on a disc, the polar-coordinate identity ∫D(c,s)F dA=∫0s∫02πF(c+teiθ) t dθ dt follows first for indicators of annular sectors and nonnegative simple functions, and then for general F by monotone convergence.

Proof

technique · direct
1.1L1L2given

Fix a compact disc D(a,R)‾⊆Ω and a smaller concentric disc D(a,ρ)‾ with 0<ρ<R. The function u is upper semicontinuous on the compact circle ∂D(a,R), so [L2] gives a finite upper bound there. By the harmonic-comparison theorem [L1], u is therefore bounded above on D(a,ρ)‾ by the harmonic majorant obtained from any continuous boundary majorant on ∂D(a,R).

1.2L2L3givenalgebra

The set A={z∈Ω:u(z)=−∞} has empty interior. Suppose instead that D(c0,R)⊆A for some R>0, and fix any point x in the connected component of Ω containing c0. By [L3], choose a polygonal path γ in that component from c0 to x. Because γ([0,1]) is compact and lies in the open set Ω, choose r>0 with 3r<R and D(y,4r)‾⊆Ω for every y∈γ([0,1]). Subdivide the path by points c0,c1,…,cN=x on γ with ∣cj+1−cj∣<r/2 for every j. We claim inductively that D(cj,3r)⊆A for all j. The case j=0 holds because 3r<R. If D(cj,3r)⊆A and b∈D(cj,7r/2), choose ρ with max⁡(0,∣b−cj∣−3r)<ρ<r/2. Then the circle ∣z−b∣=ρ lies in D(cj,4r)⊆Ω and meets D(cj,3r) in an open arc, so u=−∞ on a set of positive arc-length measure on that circle. By [L2], the circle values are Borel measurable and bounded above, hence the circle average is −∞. The submean inequality therefore gives u(b)=−∞, proving D(cj,7r/2)⊆A. Since ∣cj+1−cj∣<r/2, one has D(cj+1,3r)⊆D(cj,7r/2)⊆A, completing the induction. In particular x∈A. Because x was arbitrary in the component, this contradicts the subharmonic convention that u is not identically −∞ there. Thus A has empty interior, so every open subdisc contains a point where u is finite.

2.1step 1.1step 1.2choosealgebra

Fix a∈Ω and choose r>0 with D(a,3r)‾⊆Ω. Step 1.1, applied with outer radius 3r and inner radius 2r, gives a finite upper bound M for u on D(a,2r). By step 1.2 choose c∈D(a,r/2) with u(c)>−∞, and then choose r+∣c−a∣<s<2r−∣c−a∣. These inequalities give D(a,r)⊆D(c,s)⊆D(a,2r).

3.1step 2.1L2L4algebra

For every 0<t<s, the submean inequality at c gives ∫02π(M−u(c+teiθ)) dθ≤2π(M−u(c)). The integrand is nonnegative and Borel by [L2]. Multiply by t, integrate from 0 to s, and apply [L4] to obtain ∫D(c,s)(M−u) dA≤πs2(M−u(c))<∞. Thus the negative part of u is integrable on D(c,s), while its positive part is bounded there by M. Hence u∈L1(D(c,s)), and therefore u∈L1(D(a,r)).

4.1step 3.1∎

Every point a∈Ω admits such a disc D(a,r), so u∈Lloc1(Ω).

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

The logarithm of the modulus of a holomorphic function is subharmonic

Statement

Let Ω⊆C be a complex domain and let f be holomorphic on Ω, not identically zero on any connected component. Define u(z)=log⁡∣f(z)∣, with the convention u(z)=−∞ at the zeros of f. Then u is subharmonic on Ω.

Facts & Assumptions

Given: A holomorphic function f on a complex domain Ω, not identically zero on any connected component.

[L1]

A C2 real function is subharmonic exactly when its Laplacian is nonnegative (A C^2 function is subharmonic exactly when its Laplacian is nonnegative).

[L2]

Near a zero a of order m, the function f factors as f(z)=(z−a)mg(z) with g holomorphic and g(a)≠0 (The order of a zero is the exponent in its local holomorphic factorization).

[L3]

A holomorphic nonvanishing function on a disc has a holomorphic logarithm there (A nonvanishing holomorphic function on a disc has a holomorphic logarithm).

[L4]

Holomorphic functions are smooth, so their real and imaginary parts admit the second derivatives used in [L1] (Holomorphic functions are real analytic and smooth in their two real coordinates).

Proof

technique · direct
1.1L1L3L4

Let D⊆Ω be a disc on which f has no zeros. By [L3], there is a holomorphic function L on D with exp⁡L=f. Writing L=α+iβ, one has α=log⁡∣f∣ on D. Since L is holomorphic and smooth by [L4], the Cauchy-Riemann equations imply Δα=0, so [L1] makes log⁡∣f∣ subharmonic on every zero-free disc.

2.1L2step 1.1

Fix a zero a of f, and let m=ord⁡a(f). By [L2], on a small disc about a one has f(z)=(z−a)mg(z) with g(a)≠0. Shrinking if necessary, g has no zeros there, so step 1.1 makes log⁡∣g∣ harmonic and hence subharmonic on that disc.

3.1step 2.1algebra

On the punctured disc around a, [step 2.1, algebra] u(z)=mlog⁡∣z−a∣+log⁡∣g(z)∣. The function log⁡∣z−a∣ is harmonic on the punctured disc, and at the center a its value is −∞ while every circle average is finite; hence it is subharmonic there. Therefore the right-hand side is subharmonic on the whole disc, agreeing with u away from a and with u(a)=−∞ at the center.

4.1step 1.1step 3.1∎

Every point of Ω lies either on a zero-free disc covered by step 1.1 or on a zero-containing disc covered by step 3.1. So u is subharmonic throughout Ω.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

Positive powers of the modulus of a holomorphic function are subharmonic

Statement

Let f be holomorphic on a complex domain Ω, not identically zero on any connected component, and let p>0. Then the function z⟼∣f(z)∣p is subharmonic on Ω.

Facts & Assumptions

Given: A holomorphic function f on a complex domain Ω, not identically zero on any connected component, and a real number p>0.

[L1]

The function log⁡∣f∣, with value −∞ at the zeros of f, is subharmonic (The logarithm of the modulus of a holomorphic function is subharmonic).

Proof

technique · direct
1.1L1algebra

Put u=log⁡∣f∣. By [L1], for every closed disc D(a,r)‾⊆Ω, [L1, algebra] u(a)≤12π∫02πu(a+reit) dt. Exponentiating and using Jensen's inequality for the convex increasing map x↦epx gives ∣f(a)∣p=epu(a)≤12π∫02πepu(a+reit) dt=12π∫02π∣f(a+reit)∣p dt.

2.1step 1.1given∎

The function ∣f∣p is continuous, hence upper semicontinuous, and is not identically zero on a connected component because f is not identically zero there. Step 1.1 is exactly the submean inequality, so ∣f∣p is subharmonic.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

Positive linear combinations and finite maxima preserve subharmonicity

Statement

Let Ω⊆C be a complex domain.

  1. If u1,…,um are subharmonic on Ω and α1,…,αm≥0, then α1u1+⋯+αmum is subharmonic on Ω, where terms with αj=0 are omitted (so an all-zero combination is the zero function).
  2. If u1,…,um are subharmonic on Ω, then u(z)=max⁡{u1(z),…,um(z)} is subharmonic on Ω.

Facts & Assumptions

Given: Subharmonic functions u1,…,um on a complex domain Ω.

[L1]

Subharmonicity is equivalent to harmonic comparison on compactly contained discs (Subharmonicity is equivalent to harmonic comparison on compactly contained discs).

[L2]

The defining submean inequality for subharmonicity is linear in the function being averaged (Subharmonic functions on plane domains).

[L3]

A subharmonic function is finite almost everywhere (Plane subharmonic functions are locally integrable).

Proof

technique · direct
1.1givenL2L3algebra

Let I={j:αj>0}. If I is empty, the combination is the harmonic zero function. Otherwise it means the well-defined extended-real sum ∑j∈Iαjuj; no product 0⋅(−∞) occurs. Finite sums with positive coefficients preserve upper semicontinuity, and [L3] shows that all summands are finite simultaneously almost everywhere, so their sum is not identically −∞. On any closed disc, multiply the submean inequality for uj by αj>0 and sum over I to obtain the submean inequality for the combination.

1.2L1given

For the finite maximum, upper semicontinuity is preserved by finite maxima. Let D(a,r)‾⊆Ω and let h be continuous on the closure, harmonic on the disc, and satisfy h≥max⁡(u1,…,um) on the boundary. Then h≥uj on the boundary for every j, so [L1] gives h≥uj throughout the disc for every j. Therefore h≥max⁡(u1,…,um) on the disc. Another use of [L1] shows that the maximum is subharmonic.

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 prove the two closure properties.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

A decreasing limit of plane subharmonic functions is subharmonic or identically -infinity

Statement

Let Ω⊆C be a complex domain and let u1≥u2≥⋯ be a decreasing sequence of subharmonic functions on Ω. Put u(z)=lim⁡n→∞un(z). Then either u≡−∞ on Ω, or u is subharmonic on Ω.

Facts & Assumptions

Given: A decreasing sequence (un) of subharmonic functions on a complex domain Ω.

[L1]

The submean inequality is the defining local condition for subharmonicity (Subharmonic functions on plane domains).

[L2]

Circle boundary values of upper semicontinuous functions are Borel and bounded above, so a constant may be added to make the decreasing sequence nonnegative on a fixed circle before applying monotone convergence (Upper semicontinuous functions are Borel and their circle averages are defined).

[L3]

Monotone convergence turns an increasing sequence of nonnegative measurable functions into the limit of their integrals (Monotone convergence for the integral).

Proof

technique · direct
1.1given

A decreasing limit of upper semicontinuous functions is upper semicontinuous, so u is upper semicontinuous on Ω. If u≡−∞, the first alternative of the statement holds and there is nothing more to prove. Assume from now on that u is finite at least at one point.

1.2L1L2L3choose

Fix a closed disc D(a,r)‾⊆Ω. For every n, [L1] gives [L1, L2, L3, choose] un(a)≤12π∫02πun(a+reit) dt. By [L2], the boundary functions are measurable and bounded above. Choose a constant M larger than u1 on the circle. Then M−un(a+reit) is an increasing sequence of nonnegative measurable functions of t, so [L3] yields lim⁡n→∞12π∫02πun(a+reit) dt=12π∫02πu(a+reit) dt.

2.1step 1.1step 1.2L1∎

Passing to the limit in the inequalities of step 1.2 gives [step 1.1, step 1.2, L1] u(a)≤12π∫02πu(a+reit) dt. Since the disc was arbitrary and step 1.1 supplied upper semicontinuity, [L1] makes u subharmonic.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Upper-semicontinuous regularization

Definition

Let Ω⊆C be open and let v:Ω→[−∞,∞) be any function. Its upper-semicontinuous regularization is v∗(z):=lim sup⁡w→zv(w)=lim⁡ρ↓0sup⁡{v(w):∣w−z∣<ρ, w∈Ω}.

Remarks

The function v∗ is upper semicontinuous by construction and satisfies v≤v∗. It is the least upper-semicontinuous majorant of v: any upper-semicontinuous g with v≤g also satisfies v∗≤g.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

The upper-semicontinuous regularization of a locally bounded-above subharmonic supremum is subharmonic

Statement

Let F be a nonempty family of subharmonic functions on a complex domain Ω, and suppose that for every compact set K⊆Ω there is a real number MK with v≤MK on K for every v∈F. Define u(z)=sup⁡v∈Fv(z),U=u∗. Then U is subharmonic on Ω.

Facts & Assumptions

Given: A locally bounded-above family F of subharmonic functions on a complex domain Ω.

[L1]

Finite maxima of subharmonic functions are subharmonic (Positive linear combinations and finite maxima preserve subharmonicity).

[L2]

A function is subharmonic exactly when every harmonic boundary majorant on a compactly contained disc majorizes it throughout that disc (Subharmonicity is equivalent to harmonic comparison on compactly contained discs).

[L3]

Upper-semicontinuous regularization is the least upper-semicontinuous majorant (Upper-semicontinuous regularization).

Proof

technique · direct
1.1givenL3

For every compact set K⊆Ω, the hypothesis gives a real number MK with u≤MK on K, so both u and U=u∗ are locally bounded above and never take the value +∞. Because F is nonempty and every v∈F satisfies v≤u≤U, the function U is not identically −∞ on any connected component. By [L3], U is upper semicontinuous and satisfies u≤U.

2.1step 1.1given

Let D(a,r)‾⊆Ω and let h be continuous on the closure, harmonic on the disc, and satisfy h≥U on ∂D(a,r). Because u≤U, one also has h≥u on the boundary.

3.1L1L2step 2.1

Fix any v∈F. Since h≥v on ∂D(a,r), [L2] gives h≥v on D(a,r). The same is therefore true for every finite maximum of members of F, and [L1] keeps those maxima subharmonic. Taking the supremum over all v∈F yields h≥u on D(a,r).

4.1L2L3step 3.1∎

Since h is continuous and dominates u, it also dominates the least upper-semicontinuous majorant U by [L3]. Thus h≥U on D(a,r). Another use of [L2] shows that U is subharmonic on Ω.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

A plane subharmonic function with an interior maximum is constant on its component

Statement

Let u be subharmonic on a complex domain Ω. If u attains a finite maximum at an interior point of Ω, then u is constant on Ω.

Facts & Assumptions

Given: A subharmonic function u on a complex domain Ω and a point a∈Ω with u(a)=M=sup⁡Ωu<∞.

[L1]

Subharmonicity means that every sufficiently small circle average is at least the center value (Subharmonic functions on plane domains).

Proof

technique · direct
1.1given

Let [given] S={z∈Ω:u(z)=M}. Because u is upper semicontinuous, S is closed in Ω, and it is nonempty because a∈S.

1.2L1given

Choose r>0 with D(a,r)‾⊆Ω. For every 0<ρ<r, [L1] gives [L1, given] M=u(a)≤12π∫02πu(a+ρeit) dt≤M, so the average equals M. Since the integrand never exceeds M, it equals M almost everywhere on the circle ∣z−a∣=ρ. If some point of that circle had value <M, upper semicontinuity would make the value <M on a short arc, forcing the average below M. Hence u≡M on every circle ∣z−a∣=ρ with 0<ρ<r.

2.1step 1.1step 1.2∎

Step 1.2 shows that every point of D(a,r) lies in S, so S is open in Ω. Since Ω is connected and S is nonempty, closed, and open, one has S=Ω. Therefore u≡M on Ω.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-27Open item page →

Poisson modification on a compactly contained disc

Definition

Let u be subharmonic on a complex domain Ω, and let D=D(a,r)⋐Ω be an open disc. A boundary approximation for u on ∂D is a decreasing sequence of continuous functions ϕn:∂D→R with ϕn↓u∣∂D; such sequences exist because the circle data are upper semicontinuous by Upper semicontinuous functions are Borel and their circle averages are defined.

For each n, let hn be the harmonic function on D, continuous on D‾, with boundary values ϕn, obtained by transporting the unit-disc Poisson solution of The Poisson integral gives the unique continuous harmonic extension on the closed unit disc across the affine map z↦(z−a)/r and using Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate.

The Poisson modification of u on D is the function PDu defined by PDu(z)={inf⁡nhn(z),z∈D,u(z),z∈Ω∖D.

Remarks

The next theorem proves that the inside function inf⁡nhn is harmonic, independent of the chosen boundary approximation, and no smaller than the original subharmonic function on D.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

Subharmonic pieces glue across a boundary under the limsup inequality

Statement

Let Ω⊆C be a complex domain, let D⊆Ω be open, let u be subharmonic on Ω, and let v be subharmonic on every connected component of D. Assume that for every ζ∈∂D∩Ω, lim sup⁡z→ζz∈Dv(z)≤u(ζ). Define w(z)={max⁡{u(z),v(z)},z∈D,u(z),z∈Ω∖D. Then w is subharmonic on Ω.

Facts & Assumptions

Given: A complex domain Ω, an open subset D⊆Ω, subharmonic functions u on Ω and v on every component of D, and the boundary limsup inequality of the Statement.

[L1]

Subharmonicity is equivalent to harmonic comparison on compactly contained discs (Subharmonicity is equivalent to harmonic comparison on compactly contained discs).

[L3]

A subharmonic function attaining a finite interior maximum on a connected domain is constant (A plane subharmonic function with an interior maximum is constant on its component).

Proof

technique · direct
1.1givenL2

On D, the function w=max⁡{u,v} is subharmonic by [L2]. Away from ∂D its upper semicontinuity is therefore clear. At ζ∈∂D∩Ω, the inside limsup is at most u(ζ) by the hypothesis and upper semicontinuity of u, while the outside limsup is at most u(ζ)=w(ζ). Thus w is upper semicontinuous on Ω.

1.2L1given

Let B‾⊆Ω be a closed disc and let h be continuous on B‾, harmonic on B, and satisfy h≥w on ∂B. Because w≥u there, [L1] first gives h≥u throughout B.

2.1step 1.2L3given

Let C be a connected component of B∩D. On ∂C∩∂B one has h≥w≥v. At a boundary point of C inside B, the seam hypothesis and step 1.2 give lim sup⁡C(v−h)≤u−h≤0. Thus the subharmonic function v−h has boundary limsup at most 0 on the bounded domain C. If it were positive somewhere, upper semicontinuity and the boundary bound would make it attain a positive interior maximum, contradicting [L3]. Hence h≥v on every such component.

3.1L1step 1.1step 1.2step 2.1∎

Steps 1.2 and 2.1 give h≥u on B and h≥v on B∩D, hence h≥w throughout B. Every harmonic boundary majorant therefore majorizes w, so [L1] and step 1.1 make w subharmonic on Ω.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

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 Ω.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The Perron lower family for continuous boundary data

Definition

Let Ω⊆C be a bounded complex domain and let φ:∂Ω→R be continuous. A function v:Ω→[−∞,∞) is a Perron lower function for (Ω,φ) when:

  1. v is subharmonic on Ω;
  2. for every ζ∈∂Ω, lim sup⁡z→ζz∈Ωv(z)≤φ(ζ).

The collection of all such functions is the Perron lower family and is denoted P(φ,Ω).

Remarks

The word lower refers to the boundary condition: members of the family are subharmonic functions that stay below the prescribed boundary datum in the limsup sense.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The Perron envelope and its regularization

Definition

Let Ω be a bounded complex domain and let φ:∂Ω→R be continuous. The Perron envelope is the pointwise supremum Uφ(z):=sup⁡{v(z):v∈P(φ,Ω)},z∈Ω.

Its regularized Perron envelope is defined directly by Hφ(z):=lim⁡ρ↓0sup⁡{Uφ(w):w∈Ω, ∣w−z∣<ρ}.

Remarks

This limsup is meaningful with values in [−∞,+∞] before any boundedness theorem is used. The next lemma proves min⁡∂Ωφ≤Uφ≤max⁡∂Ωφ, so in the present Perron setting Hφ is finite-valued and is exactly the upper-semicontinuous regularization Uφ∗.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The Perron family is nonempty and uniformly bounded by the boundary data

Statement

Let Ω⊆C be a bounded complex domain and let φ:∂Ω→R be continuous. Put m=min⁡∂Ωφ,M=max⁡∂Ωφ. Then:

  1. P(φ,Ω) is nonempty;
  2. every v∈P(φ,Ω) satisfies v≤M on Ω;
  3. the constant function m belongs to P(φ,Ω), so the Perron envelope satisfies m≤Uφ≤M.

Facts & Assumptions

Given: A bounded complex domain Ω and a continuous boundary datum φ:∂Ω→R.

[L1]

The Perron lower family consists of subharmonic functions satisfying the boundary limsup inequality against φ (The Perron lower family for continuous boundary data).

[L2]

A subharmonic function on a connected domain cannot attain a finite interior maximum unless it is constant (A plane subharmonic function with an interior maximum is constant on its component).

Proof

technique · direct
1.1L1given

The constant function m is harmonic, hence subharmonic, and its boundary limsup equals m≤φ. Therefore m∈P(φ,Ω) by [L1], so the Perron family is nonempty.

1.2L1L2given

Let v∈P(φ,Ω) and fix ε>0. By the boundary limsup condition in [L1], every boundary point ζ has a neighbourhood Uζ such that v≤M+ε on Uζ∩Ω. The boundary is compact because Ω is bounded, so finitely many such neighbourhoods cover ∂Ω; their union leaves a compact set K⋐Ω. If v exceeded M+ε somewhere in Ω, then upper semicontinuity would make v attain its maximum over K at an interior point with value >M+ε, contradicting [L2] because v is not constant with that value near the boundary collar. Hence v≤M+ε on Ω.

2.1step 1.1step 1.2∎

Letting ε↓0 in step 1.2 gives v≤M on Ω for every v∈P(φ,Ω). Together with step 1.1, this yields m≤Uφ≤M.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

The regularized Perron envelope is harmonic

Statement

Let Ω⊆C be a bounded complex domain and let φ:∂Ω→R be continuous. Then the regularized Perron envelope Hφ is harmonic on Ω.

Facts & Assumptions

Given: A bounded complex domain Ω and a continuous boundary datum φ:∂Ω→R.

[L1]

The Perron family is nonempty, every lower function is bounded above by M=max⁡∂Ωφ, and the envelope satisfies m≤Uφ≤M for m=min⁡∂Ωφ (The Perron family is nonempty and uniformly bounded by the boundary data). The envelope regularization is the local limsup of Uφ (The Perron envelope and its regularization).

[L2]

Poisson modification of a lower function on an interior disc stays subharmonic, is harmonic on that disc, majorizes the original lower function, and remains in the Perron family because it is unchanged near ∂Ω (Poisson modification is subharmonic and majorizes the original function, Poisson modification on a compactly contained disc).

[L3]

Finite maxima and positive finite sums preserve subharmonicity; in particular finite maxima of Perron lower functions remain in the Perron family (Positive linear combinations and finite maxima preserve subharmonicity).

[L4]

The Poisson integral of continuous circle data uses the positive Poisson kernel. The Poisson modification is the infimum of the Poisson integrals of any decreasing continuous boundary approximation, independent of that approximation (The Poisson integral on the unit disc, The Poisson kernel is positive, has total mass one, and concentrates at a boundary point, Poisson modification on a compactly contained disc, Poisson modification is subharmonic and majorizes the original function).

[L5]

If a nonnegative harmonic function is defined on a neighbourhood of a closed disc, its value on a smaller concentric disc is at most a Harnack factor times its center value; the factor tends to 1 as the smaller radius tends to 0 (Positive harmonic functions on a disc satisfy Harnack's inequality).

[L6]

The upper-semicontinuous regularization of a locally bounded-above subharmonic supremum is subharmonic (The upper-semicontinuous regularization of a locally bounded-above subharmonic supremum is subharmonic).

[L7]

Every harmonic function has the circle mean-value property, and a continuous function with that local property is harmonic (Plane harmonic functions satisfy the mean-value property, A continuous plane function with the local mean-value property is harmonic).

[L8]

A subharmonic function that attains a finite interior maximum is constant (A plane subharmonic function with an interior maximum is constant on its component).

Proof

technique · directed-supremum argument using finite witnesses
1.1L1L6

By [L1], the Perron family P(φ,Ω) is nonempty and locally bounded above. Applying [L6] shows that Hφ is finite-valued and subharmonic on Ω, with m≤Uφ≤Hφ≤M.

2.1L1L2step 1.1

Fix a∈Ω and a disc D=D(a,R) with D‾⋐Ω. For each v∈P(φ,Ω) write hv=(PDv)∣D. By [L2], hv is harmonic on D, the globally defined PDv is again a Perron lower function, and v≤hv≤Uφ≤Hφ≤M on D. The family of these lifts is nonempty; the constant lower function m gives hm=m.

3.1L4step 2.1

The Poisson modification is order preserving: if v≤w are two lower functions, take any decreasing continuous boundary approximations αn↓v∣∂D and βn↓w∣∂D supplied by [L4]. The finite minima γn:=min⁡(αn,βn) are continuous, decrease to v∣∂D, and satisfy γn≤βn. Positivity of the Poisson kernel in [L4] makes the harmonic Poisson integrals satisfy P[γn]≤P[βn] on D. Taking their decreasing limits in the intrinsic definition of Poisson modification yields hv≤hw. This uses two witnesses and their finite minima, with no countable family of choices.

4.1L1L3step 2.1step 3.1

Given v,w in the Perron family, t=max⁡(v,w) belongs to the family by [L3], and step 3.1 gives ht≥hv,hw. Thus the lifted family is upward directed. Define h(z):=sup⁡vhv(z) on D; by step 2.1 and the constant member hm=m, it is finite and satisfies m≤h≤Hφ.

5.1L5step 4.1

We prove that h is harmonic without choosing a sequence of lifts. Fix b∈D and a closed disc D(b,Rb)‾⊂D. For any ϵ>0, the supremum defining h(b) gives one lift hv with hv(b)>h(b)−ϵ. For any other lift hw, step 4.1 gives a common upper lift ht≥hv,hw. The difference ht−hv is nonnegative harmonic on D and has value less than ϵ at b. Apply [L5] to ht−hv+δ and let δ↓0: for every r<Rb there is a finite constant Cb,r, independent of v,w,t, such that 0≤ht(z)−hv(z)≤Cb,rϵ on D(b,r)‾. Hence 0≤h(z)−hv(z)≤Cb,rϵ there after taking the supremum over w. One harmonic lift therefore approximates h uniformly on each smaller disc to any prescribed error, using only one existential witness per error.

5.2L1L2L5step 2.1step 4.1

We show h(a)=Hφ(a). Step 4.1 already gives h(a)≤Hφ(a). Fix ϵ>0. By [L1], m≤Hφ(a)≤M. Choose a radius r>0 small enough that D(a,r)‾⊂D and the Harnack upper factor C(r) from [L5] for the larger disc D satisfies (C(r)−1)(M−m+ϵ)<ϵ/2. The limsup definition in [L1] gives one point z∈D(a,r) with Uφ(z)>Hφ(a)−ϵ/4, and the supremum defining Uφ(z) gives one lower function v with v(z)>Uφ(z)−ϵ/4. By step 2.1, hv(z)≥v(z)>Hφ(a)−ϵ/2. The function M−hv is nonnegative harmonic on D; [L5], applied to M−hv+δ and then with δ↓0, gives M−hv(a)≤C(r)(M−hv(z)). Since M−hv(z)<M−m+ϵ/2, rearrangement gives hv(a)>Hφ(a)−ϵ. Consequently h(a)≥hv(a)>Hφ(a)−ϵ for every ϵ>0, so h(a)=Hφ(a). The point and lower function are chosen only for this one ϵ; no countable choice is used.

6.1L7step 5.1

The uniform approximation in step 5.1 makes h continuous: given a tolerance, choose one harmonic hv uniformly close on a neighbourhood, then use continuity of that hv and the triangle inequality. On any circle whose closed disc lies in D, approximate h uniformly on that closed disc by one hv, use the circle mean-value identity for hv from [L7], and let the error tend to 0. Thus h has the local circle mean-value property. By the converse in [L7], h is harmonic on D. This epsilon proof does not assemble the individual witnesses into a sequence.

7.1L1L3L8step 1.1step 4.1step 6.1step 5.2∎

The difference Hφ−h is subharmonic on D: Hφ is subharmonic by step 1.1, −h is harmonic and hence subharmonic by step 6.1, and [L3] preserves the sum. It is nonpositive by step 4.1 and vanishes at the interior point a by step 5.2. The maximum principle [L8] forces it to be identically zero on D. Therefore Hφ=h on D and is harmonic near a. Since a was arbitrary, Hφ is harmonic on Ω. The empty-family case is excluded by [L1], m handles the constant lower bound, and every approximation uses only finite existential choices; no choice axiom has been added to the theorem.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Barriers and regular boundary points

Definition

Let Ω⊆C be a bounded complex domain and let ζ∈∂Ω.

A barrier at ζ is a subharmonic function b:Ω→[−∞,0) such that:

  1. b(z)→0 as z→ζ with z∈Ω;
  2. for every neighbourhood V of ζ there is a constant cV<0 with lim sup⁡z→ηz∈Ωb(z)≤cV(η∈∂Ω∖V).

The boundary point ζ is regular when for every continuous boundary datum φ:∂Ω→R, the regularized Perron envelope Hφ satisfies lim⁡z→ζz∈ΩHφ(z)=φ(ζ).

Remarks

The barrier is global on Ω, but the second clause is exactly what makes a local peak function sufficient: once one is globalized, it is automatically separated from 0 away from the marked boundary point.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-27Open item page →

A boundary point is regular exactly when it admits a barrier

Statement

Let Ω⊆C be a bounded complex domain and let ζ∈∂Ω. Then ζ is regular if and only if Ω admits a barrier at ζ.

Facts & Assumptions

Given: A bounded complex domain Ω and a boundary point ζ∈∂Ω.

[L1]

The Perron lower family and its pointwise supremum Uφ define Hφ=Uφ∗ (The Perron lower family for continuous boundary data, The Perron envelope and its regularization).

[L2]

The Perron family is nonempty and bounded above for continuous boundary data; its regularized envelope is subharmonic (The Perron family is nonempty and uniformly bounded by the boundary data, The upper-semicontinuous regularization of a locally bounded-above subharmonic supremum is subharmonic).

[L3]

A barrier at ζ is a negative subharmonic function that tends to 0 at ζ and stays uniformly below a negative constant on the rest of the boundary (Barriers and regular boundary points).

[L4]

The C2 function q(z)=∣z−ζ∣2 is subharmonic because Δq=4≥0 (A C^2 function is subharmonic exactly when its Laplacian is nonnegative).

[L5]

Positive sums of subharmonic functions are subharmonic (Positive linear combinations and finite maxima preserve subharmonicity). A subharmonic function on a bounded domain whose boundary limsup is everywhere at most 0 is at most 0, by the subharmonic maximum principle (A plane subharmonic function with an interior maximum is constant on its component).

Proof

technique · direct
1.1L3given

Suppose b is a barrier at ζ, and fix a continuous boundary datum φ and ε>0. Choose a neighbourhood V of ζ such that ∣φ(η)−φ(ζ)∣<ε for η∈V∩∂Ω. By [L3] there is cV<0 bounding the boundary limsup of b on ∂Ω∖V. Since φ is bounded on the compact boundary, choose A>0 large enough that, on this complement, both φ(ζ)−ε+AcV≤φ(η) and φ(η)+AcV≤φ(ζ)+ε hold. If the complement is empty, any A>0 suffices.

1.2L1L2L3L4L5given

Conversely suppose ζ is regular. Set ψ(η)=−∣η−ζ∣2 on ∂Ω and B=Hψ. By [L2], B is subharmonic, and regularity gives B(z)→ψ(ζ)=0 as z→ζ. For any v∈P(ψ,Ω), [L4] and [L5] make v(z)+q(z) subharmonic, with boundary limsup at most ψ(η)+q(η)=0 at every η∈∂Ω. The maximum principle in [L5] gives v≤−q. Taking the supremum and regularizing preserves this bound because q is continuous: B≤−q<0 on Ω. For any neighbourhood V of ζ with nonempty boundary complement, the compact set ∂Ω∖V has δV=min⁡η∈∂Ω∖V∣η−ζ∣2>0, so the boundary limsup of B there is at most −δV. The empty-complement case is vacuous. Thus B is a barrier at ζ.

2.1L1L3L5step 1.1

The function ℓ(z)=φ(ζ)−ε+Ab(z) is subharmonic by [L5]. Near ζ its boundary limsup is at most φ(ζ)−ε≤φ(η); away from ζ the first inequality in step 1.1 gives the same bound. Thus ℓ∈P(φ,Ω) by [L1], and Hφ≥Uφ≥ℓ. Since b(z)→0 at ζ, this proves lim inf⁡z→ζHφ(z)≥φ(ζ)−ε.

3.1L1L3L5step 1.1step 2.1

Let v∈P(φ,Ω) be arbitrary. The subharmonic function s=v+Ab−φ(ζ)−ε has boundary limsup at most 0: on V∩∂Ω use lim sup⁡v≤φ(η)<φ(ζ)+ε and b<0; on the complement use the second inequality in step 1.1. By [L5], s≤0 throughout Ω. Taking the supremum over all v gives Uφ(z)≤φ(ζ)+ε−Ab(z). For any δ>0, the barrier limit gives a neighbourhood W of ζ on which b>−δ, hence Uφ<φ(ζ)+ε+Aδ on W∩Ω. Its upper-semicontinuous regularization satisfies the same weak upper bound on a smaller neighbourhood of ζ. Letting δ↓0 yields lim sup⁡z→ζHφ(z)≤φ(ζ)+ε. Together with step 2.1 and arbitrary ε, this proves regularity.

4.1step 3.1step 1.2∎

Steps 1.1–3.1 establish both implications.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

On a regular bounded plane domain, Perron's method solves the Dirichlet problem

Statement

Let Ω⊆C be a bounded complex domain such that every boundary point is regular. For every continuous boundary datum φ:∂Ω→R, the regularized Perron envelope Hφ is harmonic on Ω, extends continuously to Ω‾, agrees with φ on ∂Ω, and is the unique function with those properties.

Facts & Assumptions

Given: A bounded complex domain Ω whose every boundary point is regular, and a continuous boundary datum φ:∂Ω→R.

[L1]

The regularized Perron envelope is harmonic on Ω (The regularized Perron envelope is harmonic).

[L2]

Regularity at a boundary point means that the Perron envelope tends to the prescribed boundary datum there; barriers characterize regular points (A boundary point is regular exactly when it admits a barrier).

[L3]

A bounded-domain harmonic extension of fixed continuous boundary data is unique (The bounded plane Dirichlet problem has at most one continuous harmonic solution).

Proof

technique · direct
1.1L1L2given

By [L1], Hφ is harmonic on Ω. By the hypothesis that every boundary point is regular and the definition packaged in [L2], for every ζ∈∂Ω one has [L1, L2, given] lim⁡z→ζz∈ΩHφ(z)=φ(ζ).

2.1step 1.1given

Step 1.1 gives the boundary limits pointwise on ∂Ω, and the continuity of φ turns those limits into a continuous extension of Hφ to Ω‾ by setting the boundary values equal to φ.

3.1step 2.1L3∎

If u is any other continuous harmonic function on Ω‾ with u=φ on ∂Ω, then [L3] applied to u and the extension from step 2.1 gives u=Hφ on Ω‾. Thus Perron's method solves the Dirichlet problem uniquely on regular bounded plane domains.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

Exterior disc points and exterior cone points are regular

Statement

Let Ω⊆C be a bounded complex domain and let ζ∈∂Ω.

  1. If there is a closed disc B(c,R)‾⊆C∖Ω with ζ∈∂B(c,R), then ζ is regular.
  2. If, after a rigid motion sending ζ to 0, the domain lies locally in a sector of opening angle <π, then ζ is regular.

Facts & Assumptions

Given: A bounded complex domain Ω and a boundary point ζ∈∂Ω.

[L1]

A boundary point is regular exactly when it admits a barrier (A boundary point is regular exactly when it admits a barrier).

[L2]

A negative local subharmonic peak with a strictly negative bound on a smaller seam globalizes to a barrier (A local strict subharmonic peak function globalizes).

Proof

technique · direct
1.1L1givenconstruct

In the exterior-disc case put Φ(z)=ζ−cz−c,b(z)=Re⁡Φ(z)−1. The center c is outside Ω‾, so Φ and b are holomorphic and harmonic respectively on Ω. Moreover ∣Φ(z)∣=R/∣z−c∣<1 for z∈Ω, hence b<0, while b(z)→0 as z→ζ. On the compact set ∂Ω∖V, for any neighbourhood V of ζ, the continuous function Re⁡Φ−1 has a strictly negative maximum: equality could hold only when Φ=1, namely at z=ζ. Thus b is a global barrier and [L1] makes ζ regular.

1.2L1L2givenconstruct

In the exterior-cone case, after translation and rotation take ζ=0 and suppose that near 0 the domain lies in S={reit:0<r<r0, ∣t∣<θ},0<θ<π/2. Choose θ′ with θ<θ′<π/2, put λ=π/(2θ′), and use the branch of zλ on the larger sector ∣t∣<θ′. Then q(z)=−Re⁡(zλ) is harmonic and negative on Ω∩S, and tends to 0 at the origin. On a sufficiently small circle ∣z∣=ρ, the angular margin gives q(z)≤−ρλcos⁡(λθ)<0(z∈Ω∩∂D(0,ρ)). Thus [L2] globalizes q to a barrier, and [L1] gives regularity.

2.1step 1.1step 1.2∎

The two barrier constructions prove the two regularity criteria.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

A local strict subharmonic peak function globalizes

Statement

Let Ω⊆C be a bounded complex domain and let ζ∈∂Ω. Suppose there are a neighbourhood U of ζ and a subharmonic function q on Ω∩U such that:

  1. q(z)<0 for every z∈Ω∩U;
  2. q(z)→0 as z→ζ with z∈Ω;
  3. for some smaller neighbourhood W⋐U of ζ, one has sup⁡{q(z):z∈Ω∩∂W}<0.

Then Ω has a global barrier at ζ.

Facts & Assumptions

Given: A bounded complex domain Ω, a boundary point ζ, and local data U, W, and q as in the Statement.

[L1]

Positive scalar multiples and finite maxima of subharmonic functions are subharmonic (Positive linear combinations and finite maxima preserve subharmonicity).

[L2]

Subharmonic pieces glue across a disc boundary under the limsup inequality (Subharmonic pieces glue across a boundary under the limsup inequality).

Proof

technique · direct
1.1L1givenchoose

Choose η>0 with q≤−η on Ω∩∂W, and then choose a constant c>0 so large that cq≤−1 on Ω∩∂W. The function cq is still subharmonic on Ω∩W by [L1], remains negative there, and still tends to 0 at ζ.

2.1L1L2step 1.1

Define [L1, L2, step 1.1] b(z)={max⁡{cq(z),−1},z∈Ω∩W,−1,z∈Ω∖W. Inside Ω∩W the function is subharmonic by [L1]. On the seam ∂W one has cq≤−1, so the inside limsup is at most the outside value −1; [L2] therefore glues the inside and outside pieces into a global subharmonic function on Ω.

3.1step 2.1∎

The function b is negative on Ω, tends to 0 at ζ because near ζ the maximum chooses the cq branch, and is identically −1 outside W, so it stays uniformly below a negative constant away from ζ. Thus b is a global barrier at ζ.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

A weak local subharmonic peak function upgrades to regularity

Statement

Let Ω⊆C be a bounded complex domain and let ζ∈∂Ω. Suppose there are a neighbourhood U of ζ and a subharmonic function q on Ω∩U such that:

  1. q(z)<0 on Ω∩U;
  2. q(z)→0 as z→ζ with z∈Ω;
  3. writing q∂(η):=lim sup⁡z→ηz∈Ω∩Uq(z)(η∈Ω∩U‾), every compact set K⊆(Ω∩U‾)∖{ζ} satisfies sup⁡η∈Kq∂(η)<0.

Then ζ is regular for Ω.

Facts & Assumptions

Given: A bounded complex domain Ω, a boundary point ζ, and local data U and q as in the Statement.

[L1]

A local strict peak function globalizes to a global barrier (A local strict subharmonic peak function globalizes).

[L2]

A boundary point is regular exactly when it admits a barrier (A boundary point is regular exactly when it admits a barrier).

Proof

technique · direct
1.1givenchoose

Choose a smaller neighbourhood W⋐U of ζ. The compact seam (Ω∩W‾)∩∂W is a compact subset of (Ω∩U‾)∖{ζ}, so hypothesis 3 gives [given, choose] sup⁡η∈(Ω∩W‾)∩∂Wq∂(η)<0. Thus q is already a local strict peak function on Ω∩W.

2.1L1L2step 1.1∎

Applying [L1] to the restricted data on W yields a global barrier at ζ. Then [L2] shows that ζ is regular.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

A boundary point whose complementary component contains another point is regular

Statement

Let Ω⊆C be a bounded complex domain and let ζ∈∂Ω. If the connected component of C^∖Ω containing ζ also contains a second point, then ζ is regular for Ω.

Facts & Assumptions

Given: A bounded complex domain Ω, a boundary point ζ∈∂Ω, and a second point in the same connected component of C^∖Ω as ζ.

[L1]

For a cycle, the index is locally constant off the trace and vanishes on every connected set in the zero-index region that meets infinity (The index of a cycle is locally constant off its trace and vanishes far from it).

[L2]

A complex domain is homologically simply connected exactly when every cycle with trace in it is null-homologous there, equivalently when every holomorphic nowhere-zero function on it has a holomorphic logarithm (Null-homologous cycles and homologous cycles in an open set, Equivalent characterisations of a homologically simply connected domain).

[L3]

Harmonicity is preserved by holomorphic changes of coordinate (Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate).

[L4]

A weak local subharmonic peak function implies regularity (A weak local subharmonic peak function upgrades to regularity).

Proof

technique · direct
1.1givenconstruct

Let a≠ζ lie in the same connected component E of C^∖Ω as ζ, and let [given, construct] T(w)=w−ζw−a. This Möbius map sends ζ to 0, sends a to ∞, and maps Ω biholomorphically onto the domain Ω′=T(Ω). Its image E′=T(E) is a connected subset of C^∖Ω′ containing both 0 and ∞. Put G=C^∖E′. Then G is an open connected neighbourhood of Ω′ and 0∉G.

2.1L1L2step 1.1

Let Γ be any cycle whose trace lies in G. By [L1], the index n(Γ,⋅) is locally constant on C∖Γ∗ and vanishes on the unbounded zero-index region. The connected set E′∩C is disjoint from Γ∗, and because E′ also contains ∞, the local constancy from [L1] forces n(Γ,p)=0 for every p∈E′∩C. Since E′=C^∖G, this says exactly that Γ is null-homologous in G by [L2]. Therefore G is homologically simply connected.

2.2L2step 1.1construct

Because G is homologically simply connected and misses 0, [L2] gives a holomorphic logarithm L of the identity map on G, so exp⁡(L(w))=w for w∈G. Hence [L2, step 1.1, construct] Re⁡L(w)=log⁡∣w∣. Because T(z)→0 as z→ζ through Ω and 0∉Ω′, choose a small neighbourhood V of 0 with Ω′∩V⊆{0<∣w∣<1}. On Ω′∩V the function q(w)=Re⁡1L(w) is harmonic, negative, and tends to 0 as w→0 through Ω′, because Re⁡L(w)=log⁡∣w∣→−∞. So q is a weak local harmonic peak function at 0 for the domain Ω′.

3.1L3L4step 2.2∎

The composition q∘T is harmonic on Ω∩T−1(V) by [L3], is negative there, and tends to 0 as z→ζ through Ω. Thus q∘T is a weak local subharmonic peak function at ζ. Applying [L4] shows that ζ is regular for Ω.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

A point on a nonsingleton boundary component is regular

Statement

Let Ω⊆C be a bounded complex domain and let ζ∈∂Ω. If the connected component of ∂Ω containing ζ is not a singleton, then ζ is regular for Ω.

Facts & Assumptions

Given: A bounded complex domain Ω and a boundary point ζ∈∂Ω whose boundary component contains another point.

[L1]

If the complementary component of C^∖Ω containing ζ contains a second point, then ζ is regular (A boundary point whose complementary component contains another point is regular).

Proof

technique · direct
1.1givenchoose

Let C be the connected component of ∂Ω containing ζ, and choose a∈C with a≠ζ. Because C⊆C^∖Ω is connected, it lies in a single connected component of C^∖Ω; that component contains both ζ and a.

2.1L1step 1.1∎

Step 1.1 puts ζ under the hypothesis of [L1], so ζ is regular for Ω.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Every bounded simply connected proper plane domain is regular

Statement

Let Ω⊆C be a bounded proper complex domain whose complement in the Riemann sphere C^ is connected. Then every boundary point of Ω is regular. In the planar working convention of the batch sources, this says that every bounded simply connected proper plane domain is regular.

Facts & Assumptions

Given: A bounded proper complex domain Ω with connected complement in C^.

[L1]

If the complementary component of C^∖Ω containing a boundary point also contains another point, then that boundary point is regular (A boundary point whose complementary component contains another point is regular).

Proof

technique · direct
1.1given

Fix ζ∈∂Ω. The complement C^∖Ω is connected by hypothesis, contains ζ, and also contains ∞ because Ω is bounded and proper. Therefore the complementary component containing ζ contains a second point.

2.1L1step 1.1∎

Applying [L1] to the boundary point ζ shows that ζ is regular. Since ζ was arbitrary, every boundary point is regular.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Conformal transport of continuous Dirichlet solutions

Statement

Let Ω,Ω′⊆C be bounded regular complex domains, let F:Ω→Ω′ be a conformal bijection that extends to a homeomorphism Ω‾→Ω′‾, and let φ:∂Ω′→R be continuous. If u is the unique continuous harmonic function on Ω‾ with boundary data φ∘F∣∂Ω, then v:=u∘F−1 is the unique continuous harmonic function on Ω′‾ with boundary data φ.

Facts & Assumptions

Given: Bounded regular complex domains Ω,Ω′, a closure-homeomorphic conformal bijection F:Ω→Ω′, and a continuous boundary datum φ:∂Ω′→R.

[L1]

On a regular bounded plane domain, Perron's method gives the unique continuous harmonic solution of the Dirichlet problem (On a regular bounded plane domain, Perron's method solves the Dirichlet problem).

[L2]

Harmonicity is preserved under holomorphic changes of coordinate (Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate).

[L3]

A bounded-domain continuous harmonic extension of fixed boundary data is unique (The bounded plane Dirichlet problem has at most one continuous harmonic solution).

Proof

technique · direct
1.1L1L2given

By [L1], the source datum φ∘F∣∂Ω has a unique continuous harmonic solution u on Ω‾. Define v=u∘F−1 on Ω′. Since F−1 is holomorphic on Ω′, [L2] makes v harmonic on Ω′.

2.1step 1.1given

The homeomorphic extension of F to the closures shows that F−1 extends continuously from Ω′‾ to Ω‾. Therefore v extends continuously to Ω′‾, and for ξ∈∂Ω′ one has [step 1.1, given] v(ξ)=u(F−1(ξ))=(φ∘F)(F−1(ξ))=φ(ξ). This identifies the transported boundary values.

3.1L2L3step 2.1

Let w be any other continuous harmonic function on Ω′‾ with boundary data φ. Then w∘F is continuous on Ω‾, harmonic on Ω by [L2], and has boundary values φ∘F on ∂Ω. By [L3], one has w∘F=u on Ω‾, hence w=v on Ω′‾.

4.1step 3.1∎

Thus v=u∘F−1 is exactly the unique Dirichlet solution on Ω′ with boundary data φ.

5 · Examples, counterexamples and false statements

None yet.

Sources