Alphabeta Math
Session-authored (Fable 5 assisted)
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.

20 results · all verified · 11 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 9 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Harmonic Functions and the Poisson Integral

1 · Prerequisites

2 · Summary

The complex-analytic prerequisites already fix the two-dimensional language of harmonicity: complex-differentiability-and-cauchy-riemann supplies the Cauchy-Riemann and component formulas, analyticity-liouville-and-morera supplies smooth holomorphic functions, mean values, and Liouville, the-identity-theorem-and-the-open-mapping-theorem supplies the open-mapping and real-part maximum principles, mixed-partials-taylor-and-extrema supplies Clairaut-Schwarz, and isolated-singularities-and-laurent-series supplies the puncture-removal theorem the harmonic page later reuses.

This page defines harmonic functions, harmonic conjugates, the mean-value property, the Poisson kernel, and the Poisson integral. It proves local and global holomorphic potentials, smoothness and real analyticity, maximum and minimum principles, Dirichlet uniqueness, harmonic Liouville, the open-set identity theorem, conformal invariance, the Poisson solution of the disc Dirichlet problem, the Poisson representation formula, the converse mean-value theorem, bounded removable harmonic singularities, Harnack's inequality and convergence principle, and harmonic and holomorphic Schwarz reflection. The companion page then computes the standard concrete examples and counterexamples.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Plane harmonic functions

Definition

Let ΩC be open, and write z=x+iy for the real coordinates on C=R2. A real-valued function u:ΩR is harmonic on Ω when u is of class C2 and satisfies Laplace's equation

uxx+uyy=0

throughout Ω.

Remarks

This page is plane-specific: the Laplacian is the two-variable operator x2+y2, and later pages generalize the theory to higher dimensions.

The function is real-valued by convention. Complex-valued harmonic maps are handled componentwise by asking both real coordinates to be harmonic.

RemarkRemark: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Agreement with the earlier C^2 holomorphic-components theorem

The present definition of harmonicity is exactly the one already reached from holomorphic functions in The C2 real and imaginary parts of a holomorphic function satisfy Laplace's equation and form a harmonic-conjugate pair: when f=u+iv is holomorphic and u,v are C2, both real components satisfy uxx+uyy=0 and vxx+vyy=0. This page keeps that convention and develops the converse direction from harmonic data, rather than introducing a second notion of “harmonic component”.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

Every plane harmonic function is locally the real part of a holomorphic function

Statement

Let ΩC be open, let u:ΩR be harmonic (Plane harmonic functions), and let aΩ. Then some radius r>0 and some holomorphic function F on the disc D(a,r) satisfy

u(z)=ReF(z)(zD(a,r)).

Facts & Assumptions

Given: An open set Ω, a harmonic function u on Ω, and a point aΩ.

[L1]

If a C2 real function is harmonic, then uxiuy has continuous first partials and satisfies the Cauchy-Riemann equations, because uxx=uyy and uxy=uyx (Clairaut--Schwarz theorem for continuous second partial derivatives, Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set).

[L2]

Every holomorphic function on a homologically simply connected complex domain has a primitive, and every star-shaped plane domain is homologically simply connected (Every holomorphic function on a homologically simply connected domain has a primitive, Star-shaped plane domains are homologically simply connected).

[L3]

A real-valued holomorphic function on a domain is constant (A real-valued holomorphic function on a domain is constant).

[L4]

A complex-valued function with continuous first partials satisfying the Cauchy-Riemann equations is holomorphic (Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set).

Proof

technique · direct
1.1

Choose r>0 with D(a,r)Ω, and define g:=uxiuy on D(a,r). Since u is harmonic and C2, [L1] makes g holomorphic on D(a,r).

givenL1choose
2.1

The disc D(a,r) is star-shaped, hence homologically simply connected by [L2], so g has a primitive G there with G=g.

step 1.1L2
3.1

Write G=U+iV. Because G=g=uxiuy, one has Ux=ux and Uy=uy, so the real-valued function H:=uU has continuous first partials with Hx=Hy=0 on D(a,r). Hence the Cauchy-Riemann equations hold for H, [L4] makes H holomorphic there, and [L3] makes it constant.

step 2.1L3L4algebra
4.1

If Hc on D(a,r), then F:=G+c is holomorphic there and ReF=U+c=u.

step 3.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Harmonic conjugates

Definition

Let ΩC be open, let u:ΩR be harmonic (Plane harmonic functions), and let v:ΩR. Then v is a harmonic conjugate of u on Ω when the complex-valued function

u+iv:ΩC

is holomorphic on Ω.

Remarks

The definition is asymmetric on purpose: it singles out v as a conjugate of u, even though later the same holomorphic function shows that u is also a harmonic conjugate of v.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Harmonic conjugates exist on homologically simply connected plane domains

Statement

Let Ω be a homologically simply connected complex domain and let u:ΩR be harmonic. Then u has a harmonic conjugate on Ω (Harmonic conjugates).

Equivalently, there is a holomorphic function F:ΩC with ReF=u on Ω.

Facts & Assumptions

Given: A homologically simply connected complex domain Ω and a harmonic function u:ΩR.

[L1]

If u is harmonic, then g:=uxiuy has continuous first partials and satisfies the Cauchy-Riemann equations, because uxx=uyy and uxy=uyx (Clairaut--Schwarz theorem for continuous second partial derivatives, Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set).

[L2]

Every holomorphic function on a homologically simply connected complex domain has a primitive (Every holomorphic function on a homologically simply connected domain has a primitive).

[L3]

A real-valued holomorphic function on a domain is constant (A real-valued holomorphic function on a domain is constant).

[L4]

A complex-valued function with continuous first partials satisfying the Cauchy-Riemann equations is holomorphic (Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set).

Proof

technique · direct
1.1

Define g:=uxiuy on Ω. Since u is harmonic, [L1] makes g holomorphic on Ω.

givenL1
2.1

By [L2], the holomorphic function g has a primitive G on Ω with G=g.

step 1.1L2
3.1

Write G=U+iV. From G=g=uxiuy one gets Ux=ux and Uy=uy, so H:=uU has continuous first partials with Hx=Hy=0 on Ω. Hence the Cauchy-Riemann equations hold for H, [L4] makes H holomorphic, and [L3] makes it constant.

step 2.1L3L4algebra
4.1

If Hc on Ω, then F:=G+c is holomorphic on Ω and ReF=U+c=u. Writing F=u+iv defines a harmonic conjugate v of u on Ω.

step 3.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Two harmonic conjugates differ by a real constant

Statement

Let Ω be a complex domain, let u:ΩR be harmonic, and let v1,v2 be harmonic conjugates of u on Ω. Then v1v2 is a real constant on Ω.

Facts & Assumptions

Given: Harmonic conjugates v1,v2 of the same harmonic function u on a domain Ω.

[L1]

By definition, u+iv1 and u+iv2 are holomorphic on Ω (Harmonic conjugates).

[L2]

Sums, differences, and scalar multiples of holomorphic functions are holomorphic (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L3]

A real-valued holomorphic function on a domain is constant (A real-valued holomorphic function on a domain is constant).

Proof

technique · direct
1.1

By [L1], the functions F1:=u+iv1 and F2:=u+iv2 are holomorphic, so [L2] makes i(F1F2)=v1v2 holomorphic on Ω.

L1L2algebra
2.1

The function v1v2 is real-valued, so [L3] makes it constant on Ω.

step 1.1L3
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Plane harmonic functions are smooth and real analytic

Statement

Every plane harmonic function is of class C and is real analytic in the two real coordinates.

Facts & Assumptions

Given: A harmonic function u on an open subset ΩC.

[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]

Holomorphic functions are smooth and real analytic in their two real coordinates (Holomorphic functions are real analytic and smooth in their two real coordinates).

Proof

technique · direct
1.1

Fix aΩ. By [L1], some disc D(a,r)Ω and some holomorphic F=U+iV on that disc satisfy u=U there.

L1choose
2.1

By [L2], the coordinate map (U,V) is smooth and real analytic on D(a,r), so its first coordinate U=u is smooth and real analytic there.

step 1.1L2
3.1

Since a was arbitrary, u is smooth and real analytic on all of Ω.

step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The circle and disc mean-value properties

Definition

Let ΩC be open and let u:ΩR be continuous.

  • The circle mean-value property says that for every closed disc D(a,r)Ω with r>0, u(a)=12π02πu(a+reit)dt.
  • The disc mean-value property says that for every closed disc D(a,r)Ω with r>0, u(a)=2r20r(12π02πu(a+seit)dt)sds.

When both hold, u is said to satisfy the mean-value property on Ω.

Remarks

The disc formula is written as the average of the concentric circle averages, so it is a genuinely plane-local statement and does not need any separate area integration convention.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Plane harmonic functions satisfy the mean-value property

Statement

Every plane harmonic function satisfies both the circle and disc mean-value properties of The circle and disc mean-value properties.

Facts & Assumptions

Given: A harmonic function u on an open set Ω, a point aΩ, and a radius r>0 with D(a,r)Ω.

[L1]

Every open disc is star-shaped and therefore homologically simply connected, and every harmonic function on such a domain is the real part of a holomorphic function (Star-shaped plane domains are homologically simply connected, Harmonic conjugates exist on homologically simply connected plane domains).

[L2]

A holomorphic function equals its average on every smaller concentric circle (A holomorphic function equals its average on every circle inside a larger concentric holomorphy disc).

Proof

technique · direct
1.1

Because the closed disc D(a,r) lies in the open set Ω, choose R>r with D(a,R)Ω. The restriction of u to this disc is harmonic, so [L1] gives a holomorphic function F on D(a,R) with ReF=u there.

L1choose
2.1

For every 0<tr, applying [L2] to F on the circle of radius t and taking real parts gives u(a)=12π02πu(a+teiθ)dθ.

step 1.1L2
3.1

The circle formula of the definition is step 2.1 at t=r.

step 2.1
4.1

Multiplying the identity of step 2.1 by 2t/r2 and integrating from 0 to r gives the disc formula of the definition, because 2r20rtdt=1.

step 2.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

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

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 ReF=u on D; the real part of F has a local maximum at a, so [L2] makes F constant on D, and therefore uM on D.

L1L2
2.1

Let S:={zΩ:uM on some neighbourhood of z}. Step 1.1 gives aS, and S is open by definition. If bS, choose a disc DbΩ and a holomorphic G on Db with ReG=u there by [L1]; since SDb contains a nonempty open set on which ReG=M, both Re(GM) and Re(MG) have local maxima there, so [L2] makes G constant on Db, hence uM on Db and bS. Thus S is closed in Ω.

step 1.1L1L2
3.1

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.

step 2.1L3algebra
4.1

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.

step 3.1L4L5
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

The bounded plane Dirichlet problem has at most one continuous harmonic solution

Statement

Let Ω be a bounded complex domain, and let u,v be continuous on Ω and harmonic on Ω. If u=v on Ω, then u=v on Ω.

Facts & Assumptions

Given: A bounded complex domain Ω, continuous functions u,v on Ω, both harmonic on Ω, and equality u=v on Ω.

[L1]

For a bounded domain, a continuous harmonic function attains its maximum and minimum on the boundary unless it is constant (Maximum and minimum principles for plane harmonic functions).

Proof

technique · direct
1.1

Let w:=uv. Then w is continuous on Ω, harmonic on Ω, and satisfies w=0 on Ω.

givenalgebra
2.1

Applying [L1] to w gives supΩw=supΩw=0, so w0 on Ω; applying [L1] to w gives supΩ(w)=0, so w0 on Ω. Hence w=0 everywhere.

step 1.1L1algebra
3.1

Therefore u=v on Ω.

step 2.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

A plane harmonic function bounded above or below is constant

Statement

A harmonic function on C that is bounded above, or bounded below, is constant.

Facts & Assumptions

Given: A harmonic function u:CR.

[L1]

The plane C is star-shaped and therefore homologically simply connected, so every harmonic function on it has a harmonic conjugate (Star-shaped plane domains are homologically simply connected, Harmonic conjugates exist on homologically simply connected plane domains, Homologically simply connected complex domains).

[L2]

Every bounded entire function is constant (Liouville's theorem: every bounded entire function is constant).

Proof

technique · direct
1.1

Suppose first that u is bounded above. By [L1], choose a harmonic conjugate v and set F:=u+iv, a holomorphic function on C. Then exp(F) is entire by [L3], and its modulus is eu, which is bounded because u is. So [L2] makes exp(F) constant.

L1L2L3
2.1

Differentiating the identity exp(F)c gives 0=(exp(F))=exp(F)F. Since an exponential value is never 0, [L3] gives F=0, and [L3] again makes F constant. Therefore u=ReF is constant.

step 1.1L3
3.1

If instead u is bounded below, then u is harmonic and bounded above, so step 2.1 applied to u makes u, and therefore u, constant.

step 2.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

A plane harmonic function that vanishes on a nonempty open set vanishes everywhere on the domain

Statement

Let Ω be a complex domain and let u:ΩR be harmonic. If u=0 on some nonempty open subset of Ω, then u=0 on all of Ω.

Facts & Assumptions

Given: A complex domain Ω, a harmonic function u on Ω, and a nonempty open subset UΩ on which u=0.

[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 function is constant (Maximum principle for the real part of a holomorphic function).

Proof

technique · direct
1.1

Let S:={zΩ:u=0 on some neighbourhood of z}. Then US, so S is nonempty, and S is open by definition.

given
2.1

Let aS. By [L1], choose a disc DΩ around a and a holomorphic function F on D with ReF=u there. Since SD contains a nonempty open set on which ReF=0, both ReF and Re(F) have interior local maxima 0 on D; [L2] therefore makes both F and F constant, so u=ReF vanishes on all of D. Hence aS.

step 1.1L1L2
3.1

Thus S is closed in Ω, and [L3] makes the nonempty clopen set S equal to all of Ω. Therefore u=0 everywhere on Ω.

step 1.1step 2.1L3
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate

Statement

Let u be harmonic on an open set VC.

  1. If ϕ:UV is holomorphic on an open set U, then uϕ is harmonic on U.
  2. If ψ:UV is antiholomorphic on an open set U, then uψ is harmonic on U.

Facts & Assumptions

Given: A harmonic function u on an open set V.

[L1]

Near every point of V, 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]

Compositions of holomorphic functions are holomorphic (The chain rule for complex derivatives).

[L3]

A map is antiholomorphic exactly when its conjugate is holomorphic, and the same criterion shows that wF(w) is holomorphic whenever F is holomorphic (A conjugate difference quotient characterizes antiholomorphic maps).

Proof

technique · direct
1.1

For the holomorphic case, fix aU. By [L1], choose a neighbourhood W of ϕ(a) and a holomorphic function F on W with ReF=u there. Shrinking around a if necessary, ϕ maps that neighbourhood into W, so [L2] makes Fϕ holomorphic and Re(Fϕ)=uϕ there. Thus uϕ is harmonic near a, and since a was arbitrary it is harmonic on U.

L1L2choose
2.1

For the antiholomorphic case, fix aU and choose W and F as in step 1.1 around ψ(a). By [L3], the map ψ~(z):=ψ(z) is holomorphic on U, and the map F~(w):=F(w) is holomorphic on W:={ζ:ζW}. Therefore [L2] makes F~ψ~ holomorphic on a neighbourhood of a, and its real part is ReF~(ψ~(z))=ReF(ψ(z))=ReF(ψ(z))=u(ψ(z)). Hence uψ is harmonic near a, and therefore on U.

step 1.1L2L3
3.1

Steps 1.1 and 2.1 prove the two invariance statements.

step 1.1step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The Poisson kernel on the unit disc

Definition

For zD={z<1} and tR, the Poisson kernel of the unit disc is

P(z,eit):=1z2eitz2.

If z=reiϕ with 0r<1, then

P(z,eit)=1r212rcos(tϕ)+r2=:Pr(tϕ).

Remarks

The second formula is just the first one written in polar coordinates. It is the form used in the one-variable estimates and in Harnack's inequality.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The Poisson kernel is positive, has total mass one, and concentrates at a boundary point

Statement

For 0r<1, the Poisson kernel

Pr(θ)=1r212rcosθ+r2

has the following properties:

  1. Pr(θ)>0 for every θ;
  2. 12π02πPr(θ)dθ=1;
  3. for every δ(0,π], supδθπPr(θ)0(r1).

Facts & Assumptions

Given: A radius 0r<1.

[L1]

The Poisson kernel is the real part of the Möbius function 1+reiθ1reiθ, because multiplying numerator and denominator by 1reiθ gives the displayed quotient with real part (1r2)/(12rcosθ+r2) (The Poisson kernel on the unit disc, exp(x+iy)=ex(cosy+isiny), exp(x+iy)=ex, and eiπ+1=0).

[L2]

The function w1+rw1rw is holomorphic on the unit disc (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero) and equals its average on every unit circle by the holomorphic mean-value property (A holomorphic function equals its average on every circle inside a larger concentric holomorphy disc).

Proof

technique · direct
1.1

Since 1r2>0 and 12rcosθ+r2=(1r)2+2r(1cosθ)>0, the quotient Pr(θ) is positive for every θ.

givenalgebra
1.2

By [L2], 1=12π02π1+reiθ1reiθdθ. Taking real parts and using [L1] gives 12π02πPr(θ)dθ=1.

L1L2
2.1

If δθπ, then cosθcosδ, so 0<Pr(θ)1r212rcosδ+r2. The denominator tends to 2(1cosδ)>0 as r1, while the numerator tends to 0, so the right-hand side tends to 0, proving the uniform concentration estimate on representatives in [π,π]. Periodicity gives the equivalent formulation using circular distance from 0.

step 1.1algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The Poisson integral on the unit disc

Definition

Let φ:DR be continuous. Its Poisson integral is the function P[φ]:DR defined by

P[φ](z):=12π02πP(z,eit)φ(eit)dt,

where P(z,eit) is the Poisson kernel of The Poisson kernel on the unit disc.

If z=reiϕ, the same formula reads

P[φ](reiϕ)=12π02πPr(ϕt)φ(eit)dt.

Remarks

The boundary datum is written on the unit circle itself, not as a 2π-periodic real function. The angle variable in the integral is only a parametrization.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

Poisson integrals are harmonic on the unit disc

Statement

For every continuous boundary datum φ:DR, the Poisson integral P[φ] is harmonic on D.

Facts & Assumptions

Given: A continuous function φ:DR.

[L1]

For fixed t, the function Ht(z):=eit+zeitzφ(eit) is holomorphic on D, and the family is jointly continuous in (t,z) on [0,2π]×D; therefore F(z):=12π02πHt(z)dt is holomorphic on D (A jointly continuous finite-interval parameter integral of holomorphic functions is holomorphic).

[L2]

The real part of Ht(z) is P(z,eit)φ(eit), by the defining algebra of the Poisson kernel (The Poisson kernel on the unit disc).

Proof

technique · direct
1.1

By [L1], the parameter integral F(z)=12π02πeit+zeitzφ(eit)dt is holomorphic on D.

L1
2.1

Taking real parts under the integral and using [L2] gives ReF(z)=12π02πP(z,eit)φ(eit)dt=P[φ](z).

step 1.1L2
3.1

By [L3], the real part of the holomorphic function F is harmonic. Since step 2.1 identifies that real part with P[φ], the Poisson integral is harmonic on D.

step 1.1step 2.1L3
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The Poisson kernel is a boundary approximate identity

Statement

Let φ:DR be continuous. Then

P[φ](reiα)φ(eiα)(r1)

uniformly in αR.

Facts & Assumptions

Given: A continuous boundary datum φ:DR.

[L1]

The Poisson kernel is positive, has total mass one, and its mass away from a fixed boundary point tends uniformly to zero as r1 (The Poisson kernel is positive, has total mass one, and concentrates at a boundary point).

Proof

technique · direct
1.1

Let ε>0. By uniform continuity of φ on the compact unit circle, choose δ(0,π] such that φ(eit)φ(eiα)<ε/2 whenever the circular distance from t to α is less than δ.

givenchoose
2.1

Writing z=reiα and subtracting φ(eiα) inside the Poisson integral, positivity and total mass one from [L1] give P[φ](z)φ(eiα)12πtα<δPr(αt)ε2dt+12πtαδPr(αt)2φdt.

L1step 1.1algebra
3.1

The first integral in step 2.1 is at most ε/2 because the kernel mass is 1, and the second is at most 2φ times the far-arc mass from [L1], which is <ε/2 for all α once r is close enough to 1. Therefore P[φ](reiα)φ(eiα)<ε uniformly in α.

step 2.1L1
4.1

Since ε was arbitrary, the convergence is uniform as r1.

step 3.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

The Poisson integral gives the unique continuous harmonic extension on the closed unit disc

Statement

Let φ:DR be continuous. Then its Poisson integral P[φ] is harmonic on D, extends continuously to D, agrees with φ on D, and is the unique function with those properties.

Facts & Assumptions

Given: A continuous boundary datum φ:DR.

[L1]

The Poisson integral is harmonic on D (Poisson integrals are harmonic on the unit disc).

[L2]

The Poisson integral converges to the boundary data uniformly as r1 (The Poisson kernel is a boundary approximate identity).

[L3]

A bounded-domain continuous harmonic extension of fixed boundary data is unique (The bounded plane Dirichlet problem has at most one continuous harmonic solution).

Proof

technique · direct
1.1

By [L1], the function P[φ] is harmonic on D.

L1
1.2

For z=reiα with 0r<1, [L2] gives P[φ](reiα)φ(eiα) uniformly in α as r1. Therefore defining the boundary values of P[φ] by φ produces a continuous extension to D.

L2
2.1

If u is any other continuous harmonic function on D with u=φ on D, then [L3] applied to u and the extended Poisson integral forces u=P[φ] on D.

step 1.1step 1.2L3
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

A harmonic function is recovered from its values on any containing circle by the Poisson formula

Statement

Let u be harmonic on an open set containing the closed disc D(a,R), and let z=a+ρeiϕ with 0ρ<R. Then

u(z)=12π02πR2ρ2R22Rρcos(ϕt)+ρ2u(a+Reit)dt.

So a harmonic function on a disc is recovered from its boundary values on any larger concentric circle lying inside its domain.

Facts & Assumptions

Given: A harmonic function u on a neighbourhood of D(a,R).

[L1]

The Poisson integral gives the unique continuous harmonic extension from the unit-circle boundary to the closed unit disc (The Poisson integral gives the unique continuous harmonic extension on the closed unit disc).

[L2]

Two continuous harmonic functions on the same bounded domain with the same boundary values agree (The bounded plane Dirichlet problem has at most one continuous harmonic solution).

Proof

technique · direct
1.1

Define v(w):=u(a+Rw) on D. Then v is continuous on D, harmonic on D, and has boundary values v(eit)=u(a+Reit).

givenalgebra
2.1

By [L1], the Poisson integral of the boundary function tu(a+Reit) is a continuous harmonic function on D with the same boundary values as v; [L2] therefore makes it equal to v throughout D.

step 1.1L1L2
3.1

Evaluating step 2.1 at w=(za)/R=(ρ/R)eiϕ gives exactly the displayed formula, because the unit-disc kernel there is 1(ρ/R)212(ρ/R)cos(ϕt)+(ρ/R)2=R2ρ2R22Rρcos(ϕt)+ρ2.

step 2.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

A continuous plane function with the local mean-value property is harmonic

Statement

Let ΩC be open, and let u:ΩR be continuous. If u satisfies the local mean-value property of The circle and disc mean-value properties, then u is harmonic on Ω.

Facts & Assumptions

Given: A continuous function u:ΩR with the local mean-value property.

[L1]

The Poisson integral of continuous boundary data is the unique continuous harmonic extension to a closed disc (The Poisson integral gives the unique continuous harmonic extension on the closed unit disc).

[L2]

Harmonic functions satisfy the mean-value property (Plane harmonic functions satisfy the mean-value property).

Proof

technique · direct
1.1

Fix a closed disc D(a,R)Ω. By [L1], the boundary values tu(a+Reit) have a unique continuous harmonic Poisson extension v to D(a,R), and [L2] makes v satisfy the same mean-value property there. Put w:=uv. Then w is continuous on D(a,R), has the local mean-value property on D(a,R), and vanishes on the boundary circle.

L1L2givenalgebra
2.1

By [L3], the closed disc is compact, so w attains a maximum M and a minimum m on D(a,R). If M>0, then the boundary values being 0 force the maximum to occur at some interior point b. For a small circle centered at b, the circle mean-value property gives M=w(b) as the average of values all bounded above by M, so every value on that circle is also M. Repeating this argument on overlapping small circles shows that the set {w=M} is both open and closed in the connected disc, hence all of D(a,R); this contradicts the boundary value 0. Therefore M0.

step 1.1L3
3.1

Applying the same argument to w gives maxD(a,R)(w)0, so w0 and therefore w0 on the closed disc. Together with step 2.1 this gives w=0 on D(a,R), so u=v there.

step 2.1algebra
4.1

Since the closed disc was arbitrary and v is harmonic on its interior, u is harmonic on every point of Ω, hence on all of Ω.

step 1.1step 3.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

A bounded harmonic function near an isolated puncture extends harmonically

Statement

Let u be harmonic on a punctured disc 0<za<R, and suppose u is bounded there. Then there is a harmonic function U on za<R whose restriction to the punctured disc is u.

Facts & Assumptions

Given: A harmonic function u on 0<za<R and a bound u(z)M there.

[L1]

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

[L2]

If F is holomorphic on a disc and FB on a concentric circle of radius ρ, then F(z0)B/ρ at the centre z0 of the smaller disc (Cauchy estimates on a smaller concentric disc).

[L3]

A holomorphic function on a punctured disc extends holomorphically across the centre as soon as it is bounded on some punctured neighbourhood of that centre (Characterizations of removable singularities).

[L4]

A holomorphic function with a zero at a factors as (za)q(z) with q holomorphic near a (The order of a zero is the exponent in its local holomorphic factorization).

[L5]

A star-shaped disc is homologically simply connected, so every holomorphic function on it has a primitive (Star-shaped plane domains are homologically simply connected, Every holomorphic function on a homologically simply connected domain has a primitive).

[L6]
[L7]

A complex-valued function with continuous first partials satisfying the Cauchy-Riemann equations is holomorphic, and a real-valued holomorphic function on a domain is constant (Continuous first partial derivatives and the Cauchy–Riemann equations imply complex differentiability pointwise, and holomorphy when they hold throughout an open set, A real-valued holomorphic function on a domain is constant).

[L9]

The fundamental theorem of calculus on a real interval rewrites a function difference as the integral of its derivative (The second fundamental theorem: if G is differentiable on [a,b] with G=f and f is integrable, then abf=G(b)G(a)).

Proof

technique · direct
1.1

Fix z0 with 0<z0a<R/2, and let ρ:=z0a/4. Then the disc D(z0,2ρ) lies in 0<za<R. By [L1], choose a holomorphic function F on D(z0,2ρ) with ReF=u there.

L1choose
2.1

The function H:=exp(F) is holomorphic on D(z0,2ρ) by [L6], and its modulus is H=eueM there by the bound on u. Applying [L2] on the circle of radius ρ about z0 gives H(z0)eM/ρ=4eM/z0a. Since H=Fexp(F) and exp(F(z0))=eu(z0)eM, one gets F(z0)4e2Mz0a.

step 1.1L2L6algebra
3.1

On every local potential disc from step 1.1 one has F=uxiuy, so g:=uxiuy is holomorphic on the punctured disc. Because the point z0 of step 1.1 was arbitrary in 0<z0a<R/2, step 2.1 yields (za)g(z)4e2M throughout 0<za<R/2. Therefore h(z):=(za)g(z) is holomorphic on 0<za<R and bounded on the punctured neighbourhood 0<za<R/2, so [L3] extends it holomorphically across a; write c:=h(a).

step 2.1L3algebra
4.1

Because hc is holomorphic on D(a,R) and vanishes at a, [L4] gives a holomorphic function k on D(a,R) with h(z)c=(za)k(z). Hence g(z)=c/(za)+k(z) on the punctured disc. Restricting to the real ray z=a+t with t>0, the identity ux(a+t)=Reg(a+t)=Re(c)/t+Rek(a+t) and [L9] imply u(a+t0)u(a+t)=Re(c)log ⁣t0t+tt0Rek(a+s)ds. Because u is bounded and k is continuous near a, the logarithmic term cannot diverge; hence Re(c)=0.

step 3.1L4L9algebra
5.1

For 0<r<R, parameterize the circle by γr(t)=a+reit. Since uγr is C1 and periodic, 0=u(γr(2π))u(γr(0))=02πddtu(γr(t))dt=Reγrg(z)dz. Writing g=c/(za)+k(z), the holomorphic function k has a primitive on D(a,R) by [L5], so its circle integral is 0; therefore 0=Re(2πic), which means Im(c)=0. Combined with step 4.1, this gives c=0.

step 3.1step 4.1L5algebra
6.1

Step 5.1 shows h(a)=0, so [L4] gives a holomorphic extension g on D(a,R) with h(z)=(za)g(z). Since the disc is star-shaped, [L5] gives a primitive G of g on D(a,R). On the punctured disc, H:=uReG has continuous first partials with Hx=Hy=0, so [L7] makes H holomorphic there; being real-valued, H is constant by [L7]. Therefore some real constant b makes u=ReG+b on the punctured disc. Since G is holomorphic on the full disc, [L8] makes U:=ReG+b harmonic on D(a,R), and this U extends u.

step 5.1L4L5L7L8
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

Positive harmonic functions on a disc satisfy Harnack's inequality

Statement

Let u be positive and harmonic on a neighbourhood of D(a,R), and let z satisfy za=ρ<R. Then

RρR+ρu(a)u(z)R+ρRρu(a).

In particular, for every r<R, the values of u on D(a,r) are bounded above and below by fixed multiples of u(a).

Facts & Assumptions

Given: A positive harmonic function u on a neighbourhood of D(a,R) and a point z=a+ρeiϕ with 0ρ<R.

[L1]

The Poisson representation on the radius-R circle is u(z)=12π02πR2ρ2R22Rρcos(ϕt)+ρ2u(a+Reit)dt (A harmonic function is recovered from its values on any containing circle by the Poisson formula).

[L2]

The center value is the average on the radius-R circle: u(a)=12π02πu(a+Reit)dt (Plane harmonic functions satisfy the mean-value property).

Proof

technique · direct
1.1

For every t, the denominator in [L1] lies between (Rρ)2 and (R+ρ)2, so the Poisson kernel there satisfies RρR+ρR2ρ2R22Rρcos(ϕt)+ρ2R+ρRρ.

givenalgebra
2.1

Multiplying the bounds of step 1.1 by the positive boundary values u(a+Reit) and integrating, [L1] and [L2] give RρR+ρu(a)u(z)R+ρRρu(a).

step 1.1L1L2
3.1

The constants in step 2.1 depend only on ρ/R, so the same bound holds for every zar<R after replacing ρ by r.

step 2.1algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26Open item page →

An increasing harmonic sequence converges locally uniformly to a harmonic limit or diverges to +infinity

Statement

Let (un) be an increasing sequence of harmonic functions on a complex domain Ω. Then exactly one of the following holds:

  1. un(z)+ for every zΩ;
  2. there is a harmonic function u on Ω such that unu locally uniformly on Ω.

Facts & Assumptions

Given: An increasing sequence (un) of harmonic functions on a complex domain Ω.

[L1]

Positive harmonic functions on a disc satisfy the Harnack inequality (Positive harmonic functions on a disc satisfy Harnack's inequality).

[L2]

Harmonic functions satisfy the mean-value property, and continuous functions with the local mean-value property are harmonic (Plane harmonic functions satisfy the mean-value property, A continuous plane function with the local mean-value property is harmonic).

[L4]

Proof

technique · direct
1.1

If un(z)+ for every zΩ, then the first alternative holds and there is nothing to prove. Assume from now on that some aΩ has (un(a)) bounded above; since the sequence is increasing, [L4] says that un(a) converges to a finite real L.

givenL4
2.1

Let KΩ be compact. By [L3], every point of K can be joined to a by a polygonal path in Ω; compactness yields finitely many discs with compact closure in Ω whose overlaps form a chain from a to a neighbourhood of each point of K. Applying [L1] to the positive harmonic differences umun on each disc, one after another along the chain, bounds supK(umun) by a constant multiple of (um(a)un(a)). Since the latter tends to 0, the sequence is uniformly Cauchy on K.

step 1.1L1L3
3.1

By step 2.1, (un(z)) is Cauchy for every z, so [L4] defines u(z):=limnun(z). The same uniform-Cauchy estimate makes the convergence locally uniform, hence u is continuous. Passing the circle mean-value identity of [L2] to the limit on every closed disc inside Ω shows that u still has the local mean-value property, and [L2] makes u harmonic.

step 2.1L2L4
4.1

Thus, if the first alternative fails, the second holds. The two alternatives are exclusive because a locally uniform limit on any disc is finite there.

step 1.1step 3.1
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-26Open item page →

Harmonic and holomorphic Schwarz reflection across the real axis

Statement

Write

D+:={zC:z<1, Imz>0}.

  1. If u is harmonic on D+, continuous on D+, and u(x)=0 for every x(1,1), then the odd reflection U(z):={u(z),Imz0,u(z),Imz<0, is harmonic on the full unit disc.
  2. If f is holomorphic on D+, continuous on D+, and real-valued on (1,1), then the reflected function F(z):={f(z),Imz0,f(z),Imz<0, is holomorphic on the full unit disc.

Facts & Assumptions

Given: The upper half-disc D+.

[L1]

The Poisson integral gives the unique continuous harmonic extension of continuous boundary data on a closed disc, and uniqueness holds on bounded domains with fixed boundary values (The Poisson integral gives the unique continuous harmonic extension on the closed unit disc, The bounded plane Dirichlet problem has at most one continuous harmonic solution).

[L2]

On a star-shaped domain, every harmonic function has a harmonic conjugate, and a real-valued holomorphic function on a domain is constant (Star-shaped plane domains are homologically simply connected, Harmonic conjugates exist on homologically simply connected plane domains, A real-valued holomorphic function on a domain is constant).

Proof

technique · direct
1.1

For the harmonic statement, let u satisfy the hypotheses, and define continuous boundary data Φ on the unit circle by taking the upper semicircle values of u and extending them oddly across the real axis. By [L1], Φ has a harmonic Poisson extension H to the full unit disc. On the upper half-disc, H and u are continuous harmonic functions with the same boundary values on the upper semicircle and on the diameter (1,1), so [L1] makes them equal there. By the odd construction of Φ, the same harmonic function satisfies H(z)=u(z) on the lower half-disc. Thus H is exactly the reflected function U, so U is harmonic.

L1
2.1

For the holomorphic statement, write f=u+iv on D+. Since f is real-valued on (1,1), one has v=0 there; applying step 1.1 to v gives a harmonic function V on the full disc that equals v above the axis and v(z) below it. Because the disc is star-shaped, [L2] gives a harmonic conjugate W of V, so V+iW is holomorphic. Multiplying by i shows that G:=W+iV is holomorphic and has imaginary part V.

step 1.1L2algebra
3.1

On D+, the holomorphic functions G and f have the same imaginary part v, so their difference is real-valued and holomorphic; [L2] makes Gf a real constant there. Subtracting that constant from G, we may assume G=f on D+.

step 2.1L2
4.1

For Imz<0, the functions G(z) and f(z) have the same imaginary part v(z). Their difference is therefore real-valued and holomorphic on the lower half-disc, hence constant by [L2]; continuity across the diameter, where both functions equal the same real boundary values, forces that constant to be 0. So G(z)=f(z) below the axis, and the reflected function F is holomorphic on the full disc.

step 3.1L2

5 · Examples, counterexamples and false statements

None yet.

Sources