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.
Maximum and minimum principles for plane harmonic functions
Statement
Let be a complex domain and let be harmonic.
- If has an interior local maximum or an interior local minimum, then is constant on .
- If is bounded and extends continuously to , then
Facts & Assumptions
Given: A harmonic function on a complex domain .
Near every point of , the function is the real part of a holomorphic function (Every plane harmonic function is locally the real part of a holomorphic function).
If the real part of a holomorphic function has an interior local maximum, then the holomorphic function is constant (Maximum principle for the real part of a holomorphic function).
A complex domain is a nonempty connected open subset of (A complex domain is a nonempty connected open subset of ).
A continuous real-valued function on a nonempty compact space attains a maximum and a minimum (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, claim 2).
Proof
Suppose has an interior local maximum at , with value . By [L1], some disc and some holomorphic on satisfy on ; the real part of has a local maximum at , so [L2] makes constant on , and therefore on .
Let . Step 1.1 gives , and is open by definition. If , choose a disc and a holomorphic on with there by [L1]; since contains a nonempty open set on which , both and have local maxima there, so [L2] makes constant on , hence on and . Thus is closed in .
Because is connected by [L3], the nonempty set that is open and closed in must equal . Thus a local interior maximum forces to be constant on . Applying the same argument to , which is harmonic because , gives the local minimum statement as well.
Now assume is bounded and is continuous on . The closure is nonempty, closed and bounded in , hence compact by [L4], so [L5] says that the continuous extension of attains a maximum and a minimum there. If either extremum were attained at an interior point and were nonconstant, step 3.1 would force to be constant. Therefore both extremal values are realized on , and the displayed equalities follow.
Depends on
Plane harmonic functions
Every plane harmonic function is locally the real part of a holomorphic function
Maximum principle for the real part of a holomorphic function
A complex domain is a nonempty connected open subset of
Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism