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
- The punctured disc has an irregular boundary point and a continuous boundary datum with no harmonic solution Counterexample
- FALSE: a nonconstant subharmonic function can attain a finite interior maximum False statement
- A dipole Green function exists on a Riemann surface Lemma
- A simply connected Greenian Riemann surface is a disc Lemma
- A simply connected surface without a Green kernel is plane or sphere Lemma
- A smooth psh exhaustion gives Hartogs pseudoconvexity on bounded domains Lemma
- Green envelope dichotomy, logarithmic pole and leastness on a Riemann surface Lemma
- Locality of subharmonicity in the plane and on Riemann surfaces Lemma
- Regular exhaustion and Dirichlet solutions on relatively compact surface domains Lemma
- Removing a compact chart disc gives a Greenian surface Lemma
- Subharmonic pieces glue across a boundary under the limsup inequality Lemma
- Symmetry of the canonical surface Green kernel 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
- Green function at infinity from the equilibrium potential Theorem
- Hartogs pseudoconvexity implies Levi pseudoconvexity for C² domains Theorem
- Maximum principle for plurisubharmonic functions 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)