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.

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

Depends on

Used by

Dependency tree · two levels

14 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