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 be subharmonic on a complex domain . If attains a finite maximum at an interior point of , then is constant on .
Facts & Assumptions
Given: A subharmonic function on a complex domain and a point with .
Subharmonicity means that every sufficiently small circle average is at least the center value (Subharmonic functions on plane domains).
Proof
Let [given] Because is upper semicontinuous, is closed in , and it is nonempty because .
Choose with . For every , [L1] gives [L1, given] so the average equals . Since the integrand never exceeds , it equals almost everywhere on the circle . If some point of that circle had value , upper semicontinuity would make the value on a short arc, forcing the average below . Hence on every circle with .
Step 1.2 shows that every point of lies in , so is open in . Since is connected and is nonempty, closed, and open, one has . Therefore on .
Depends on
Used by
- FALSE: a nonconstant subharmonic function can attain a finite interior maximum False statement
- Subharmonic pieces glue across a boundary under the limsup inequality Lemma
- The Perron family is nonempty and uniformly bounded by the boundary data Lemma
- A boundary point is regular exactly when it admits a barrier Theorem
- Subharmonicity is equivalent to harmonic comparison on compactly contained discs Theorem
- The regularized Perron envelope is harmonic Theorem
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
- Boris Khoruzhenko, Potential Theory lecture notes (standard reference, not scraped)