Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26
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 u:Ω→R be harmonic.

  1. If u has an interior local maximum or an interior local minimum, then u is constant on Ω.
  2. If Ω is bounded and u extends continuously to Ω‾, then sup⁡Ω‾u=sup⁡∂Ωu,inf⁡Ω‾u=inf⁡∂Ωu.

Facts & Assumptions

Given: A harmonic function u on a complex domain Ω.

[L1]

Near every point of Ω, the function u is the real part of a holomorphic function (Every plane harmonic function is locally the real part of a holomorphic function).

[L2]

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

[L3]

A complex domain is a nonempty connected open subset of C (A complex domain is a nonempty connected open subset of C).

Proof

technique · direct
1.1L1L2

Suppose u has an interior local maximum at a∈Ω, with value M=u(a). By [L1], some disc D⊆Ω and some holomorphic F on D satisfy Re⁡F=u on D; the real part of F has a local maximum at a, so [L2] makes F constant on D, and therefore u≡M on D.

2.1step 1.1L1L2

Let S:={ z∈Ω:u≡M on some neighbourhood of z }. Step 1.1 gives a∈S, and S is open by definition. If b∈S‾, choose a disc Db⊆Ω and a holomorphic G on Db with Re⁡G=u there by [L1]; since S∩Db contains a nonempty open set on which Re⁡G=M, both Re⁡(G−M) and Re⁡(M−G) have local maxima there, so [L2] makes G constant on Db, hence u≡M on Db and b∈S. Thus S is closed in Ω.

3.1step 2.1L3algebra

Because Ω is connected by [L3], the nonempty set S that is open and closed in Ω must equal Ω. Thus a local interior maximum forces u to be constant on Ω. Applying the same argument to −u, which is harmonic because (−u)xx+(−u)yy=−(uxx+uyy)=0, gives the local minimum statement as well.

4.1step 3.1L4L5∎

Now assume Ω is bounded and u is continuous on Ω‾. The closure Ω‾ is nonempty, closed and bounded in R2, hence compact by [L4], so [L5] says that the continuous extension of u attains a maximum and a minimum there. If either extremum were attained at an interior point and u were nonconstant, step 3.1 would force u to be constant. Therefore both extremal values are realized on ∂Ω, and the displayed equalities follow.

Depends on

Used by

Dependency tree · two levels

57 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