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.

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

Depends on

Used by

Dependency tree · one level

1 result within one dependency step 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