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.

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.

Depends on

Used by

Dependency tree · two levels

27 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