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.

A bounded harmonic function near an isolated puncture extends harmonically

Statement

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

Facts & Assumptions

Given: A harmonic function u on 0<∣z−a∣<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 ∣F∣≤B 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 (z−a)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.1L1choose

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

2.1step 1.1L2L6algebra

The function H:=exp⁡(F) is holomorphic on D(z0,2ρ) by [L6], and its modulus is ∣H∣=eu≤eM there by the bound on u. Applying [L2] on the circle of radius ρ about z0 gives ∣H′(z0)∣≤eM/ρ=4eM/∣z0−a∣. Since H′=F′exp⁡(F) and ∣exp⁡(−F(z0))∣=e−u(z0)≤eM, one gets ∣F′(z0)∣≤4e2M∣z0−a∣.

3.1step 2.1L3algebra

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

4.1step 3.1L4L9algebra

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

5.1step 3.1step 4.1L5algebra

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/(z−a)+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.

6.1step 5.1L4L5L7L8∎

Step 5.1 shows h(a)=0, so [L4] gives a holomorphic extension g on D(a,R) with h(z)=(z−a)g(z). Since the disc is star-shaped, [L5] gives a primitive G of g on D(a,R). On the punctured disc, H:=u−Re⁡G 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=Re⁡G+b on the punctured disc. Since G is holomorphic on the full disc, [L8] makes U:=Re⁡G+b harmonic on D(a,R), and this U extends u.

Depends on

Used by

Dependency tree · two levels

79 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