Alphabeta Math
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.

✓ 17 results · all verified · 8 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.

The Hartogs Phenomena

1 · Prerequisites

2 · Summary

This page records the first genuinely several-variable phenomena that fail in one complex variable. The opening route is local: Hartogs figures, slice Laurent coefficients, and the vanishing of the negative part give extension from a Hartogs figure to its bidisc hull, and the same mechanism shows that isolated punctures in complex dimension at least two are removable and that locally bounded holomorphic functions extend across a coordinate hyperplane.

The second route is global. Separate holomorphy is converted into joint holomorphy through the Baire-plus-Hartogs-lemma coefficient argument, then Hartogs figures are propagated across shell neighborhoods and glued under the explicit component-overlap hypothesis built into the finite shell cover. The final extension theorem records that restricted compact-hole argument rather than a general unrestricted Kugelsatz. The false statements isolate the points where the one-variable intuition breaks: isolated poles and essential singularities disappear, punctured several-variable domains need not force unboundedness, and domains in C2 can fail to be domains of holomorphy.

3 · Logical flowchart

4 · Definitions, theorems and proofs

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

Holomorphic extension and domains of holomorphy in several variables

Definition

Let Ω,Ω~⊆Cm be domains with Ω∩Ω~≠∅, and let f:Ω→C be holomorphic (Holomorphic functions on an open subset of Cm).

A holomorphic function f~:Ω~→C is a holomorphic extension of f to Ω~ when there is a nonempty open set W⊆Ω∩Ω~ such that f~=f on W.

A domain Ω is a domain of holomorphy when there do not exist domains U1,U2⊆Cm with

∅≠U1⊆U2∩Ω,U2⊈Ω,

such that every holomorphic f∈O(Ω) admits a holomorphic extension Ff∈O(U2) satisfying Ff=f on U1.

Remarks

This page uses the simultaneous-extension convention. To show that a domain is not a domain of holomorphy it is enough to find one fixed overlap U1⊆U2∩Ω from which every holomorphic function on Ω extends to U2. The continuation is part of the datum for each function, but the witnessing pair U1,U2 is common.

Agreement propagates only on a common connected domain. If two holomorphic functions are both defined on one connected domain and agree on a nonempty open subset, the several-variable identity theorem forces agreement there. In the definition above, however, Ω∩Ω~ can be disconnected: agreement on one component need not imply agreement on another. The witnessing overlap W is therefore part of the extension datum and cannot in general be changed arbitrarily.

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

The Hartogs figure H(r,s) and its bidisc hull

Definition

Fix real numbers 0<r,s<1. The Hartogs figure H(r,s)⊆C2 is

H(r,s):={(z1,z2):∣z1∣<1, ∣z2∣<s}∪{(z1,z2):r<∣z1∣<1, ∣z2∣<1}.

Its bidisc hull is the full unit bidisc

H^(r,s):={(z1,z2):∣z1∣<1, ∣z2∣<1}=Δ1(0)×Δ1(0).

Remarks

The first piece is the thin cylinder over the z1-disc, and the second piece is the thick outer shell in the z1-variable with full z2-disc available. The missing core is {(z1,z2):∣z1∣≤r, s≤∣z2∣<1}, and the Hartogs phenomenon is that holomorphic functions on H(r,s) do not feel that missing core.

Translated and rescaled versions are obtained by applying affine complex coordinate changes to the bidisc description above; the later shell-extension lemma uses exactly that coordinate model.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-27Open item page →

Laurent coefficients on Hartogs slices depend holomorphically on the remaining variables

Statement

Fix 0<r,s<1, let f be holomorphic on H(r,s), and choose ρ with r<ρ<1. For each integer n and each w with ∣w∣<1, define

an(w):=12πi∫∣ζ∣=ρf(ζ,w)ζn+1 dζ.

Then every an is holomorphic on the unit disc {∣w∣<1}. Moreover, for each fixed w with ∣w∣<1 the slice z↦f(z,w) has Laurent expansion

f(z,w)=∑n∈Zan(w)zn(r<∣z∣<1).

Facts & Assumptions

Given: Real numbers 0<r<s<1 are not assumed; only 0<r,s<1, a function f∈O(H(r,s)), and a radius ρ with r<ρ<1.

[L1]

The Hartogs figure contains every point (ζ,w) with ∣ζ∣=ρ and ∣w∣<1 (The Hartogs figure H(r,s) and its bidisc hull).

[L2]

A contour integral of a jointly continuous integrand that is holomorphic in the parameter variable defines a holomorphic function of that parameter (A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic).

[L3]

The Laurent coefficients of a one-variable holomorphic function on an annulus are given by the contour integral formula, and those coefficients are unique (Laurent coefficients are given by contour integrals and are unique).

Proof

technique · direct
1.1L1L2

Fix an integer n. By [L1], for ∣ζ∣=ρ and ∣w∣<1 the point (ζ,w) lies in H(r,s), so the integrand (ζ,w)↦f(ζ,w)ζ−n−1 is continuous on the circle times the unit disc and, for fixed ζ, holomorphic in w. Therefore [L2] makes an holomorphic on {∣w∣<1}.

1.2L1L3

Fix w with ∣w∣<1. Then the slice z↦f(z,w) is holomorphic on the annulus r<∣z∣<1, again by [L1]. Applying [L3] to that one-variable slice on the circle ∣z∣=ρ shows that its Laurent coefficients are exactly the numbers an(w) defined above.

2.1step 1.1step 1.2∎

The Laurent expansion from step 1.2 is therefore f(z,w)=∑n∈Zan(w)zn for r<∣z∣<1, and step 1.1 gives the holomorphic dependence of every coefficient on w.

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

Negative Laurent coefficients vanish on a Hartogs figure

Statement

In the notation of Laurent coefficients on Hartogs slices depend holomorphically on the remaining variables, one has

an(w)=0for every n<0 and every ∣w∣<1.

Facts & Assumptions

Given: A holomorphic function f on H(r,s), a radius ρ with r<ρ<1, and the Laurent coefficient functions an defined in the preceding lemma.

[L1]

Each an is holomorphic on the unit disc, and for fixed w the numbers an(w) are the Laurent coefficients of the slice z↦f(z,w) on the annulus r<∣z∣<1 (Laurent coefficients on Hartogs slices depend holomorphically on the remaining variables).

[L2]

A holomorphic function on a punctured disc has a removable singularity exactly when its Laurent expansion has no negative powers (Characterizations of removable singularities).

[L3]

A holomorphic function on a connected open set that vanishes on a nonempty open subset vanishes identically (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

Proof

technique · direct
1.1L1L2

Fix w with ∣w∣<s. Then (z,w)∈H(r,s) for every ∣z∣<1, so the slice z↦f(z,w) is holomorphic on the whole unit disc. By [L1], the coefficients an(w) are the Laurent coefficients of that slice on r<∣z∣<1, and [L2] therefore forces an(w)=0 for every n<0.

2.1step 1.1L3

For each fixed n<0, step 1.1 shows that the holomorphic function an is zero on the nonempty open disc {∣w∣<s}. The domain {∣w∣<1} is connected, so [L3] gives an≡0 there.

3.1step 2.1∎

As n<0 was arbitrary, every negative Laurent coefficient vanishes on the whole parameter disc {∣w∣<1}.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-27Open item page →

A holomorphic function on a Hartogs figure extends to the full bidisc

Statement

Fix 0<r,s<1. Every holomorphic function on the Hartogs figure H(r,s) admits a unique holomorphic extension to the bidisc H^(r,s).

Facts & Assumptions

Given: A holomorphic function f on H(r,s).

[L1]

The Hartogs figure H(r,s) and its bidisc hull H^(r,s) are the sets defined on the page's opening definition (The Hartogs figure H(r,s) and its bidisc hull).

[L2]

For any ρ with r<ρ<1, define Fρ(z,w):=12πi∫∣ζ∣=ρf(ζ,w)ζ−z dζ for ∣z∣<ρ and ∣w∣<1.

[L3]

If ∣w∣<s, then the slice z↦f(z,w) is holomorphic on the whole unit disc, so the one-variable Cauchy formula recovers it from the circle ∣ζ∣=ρ whenever ∣z∣<ρ<1 (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[L4]

A holomorphic function on a connected open set is determined by its values on any nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L5]

The negative Laurent coefficients of the z-slices vanish identically on the parameter disc (Negative Laurent coefficients vanish on a Hartogs figure), and the coefficient functions themselves are holomorphic in the parameter (Laurent coefficients on Hartogs slices depend holomorphically on the remaining variables).

[L6]

A separately holomorphic function that is locally bounded is jointly holomorphic (Locally bounded and separately holomorphic implies holomorphic).

Proof

technique · direct
1.1L1L2L6algebra

Fix ρ with r<ρ<1 and define Fρ by the Cauchy integral in [L2]. Since ∣ζ∣=ρ and ∣w∣<1 place (ζ,w) inside H(r,s) by [L1], the integral is well defined. For fixed z with ∣z∣<ρ, [L2] applied to the one complex parameter w makes w↦Fρ(z,w) holomorphic on ∣w∣<1. For fixed w, the same theorem applied to the one complex parameter z makes z↦Fρ(z,w) holomorphic on ∣z∣<ρ. The ML estimate gives local bounds on compact subsets, so [L6] upgrades Fρ to a jointly holomorphic function on {∣z∣<ρ, ∣w∣<1}.

2.1L3step 1.1

If ∣w∣<s, then the slice z↦f(z,w) is holomorphic on ∣z∣<1. Therefore [L3] gives Fρ(z,w)=f(z,w) whenever ∣z∣<ρ and ∣w∣<s. So Fρ extends f across the missing core over that open overlap.

3.1step 1.1step 2.1L4

If r<ρ1<ρ2<1, then both Fρ1 and Fρ2 are holomorphic on {∣z∣<ρ1, ∣w∣<1} by step 1.1, and step 2.1 shows that they agree on the nonempty open subset {∣z∣<ρ1, ∣w∣<s}. Hence [L4] forces Fρ1=Fρ2 on the whole connected domain {∣z∣<ρ1, ∣w∣<1}.

4.1step 3.1construct

For each point (z,w)∈H^(r,s) choose any ρ with max⁡{r,∣z∣}<ρ<1, and set F(z,w):=Fρ(z,w). Step 3.1 shows that this does not depend on the chosen ρ, so F is well defined and holomorphic locally, hence holomorphic on all of H^(r,s).

5.1step 2.1step 4.1L4

Step 2.1 gives F=f on the open set {∣w∣<s}⊆H(r,s), so F is a holomorphic extension of f to the bidisc. If G is another such extension, then F and G are holomorphic on the connected bidisc and agree on the same nonempty open overlap with f; [L4] gives F=G. Thus the extension is unique.

6.1L5step 5.1∎

The Laurent-coefficient view in [L5] is compatible with the integral construction above: the Cauchy kernel removes the vanished negative part and rebuilds the same holomorphic continuation.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-27Open item page →

A domain containing a Hartogs figure but not its hull is not a domain of holomorphy

Statement

Let Ω⊆C2 be a domain. If there exist 0<r,s<1 such that

H(r,s)⊆Ω⊆H^(r,s)andΩ≠H^(r,s),

then Ω is not a domain of holomorphy.

Facts & Assumptions

Given: A domain Ω with H(r,s)⊆Ω⊆H^(r,s) and Ω≠H^(r,s).

[L1]

A domain of holomorphy is defined by the nonexistence of one fixed overlap from which every holomorphic function extends farther (Holomorphic extension and domains of holomorphy in several variables).

[L2]

Every holomorphic function on H(r,s) extends uniquely to the full bidisc H^(r,s) (A holomorphic function on a Hartogs figure extends to the full bidisc).

Proof

technique · direct
1.1givenL2

Let f∈O(Ω). Its restriction to the open subset H(r,s) is holomorphic, so [L2] gives a holomorphic function Ff∈O(H^(r,s)) with Ff=f on H(r,s).

2.1step 1.1given

The domain H^(r,s) is not contained in Ω by hypothesis, and H(r,s) is a nonempty open subset of Ω∩H^(r,s). Thus the same open overlap works for every holomorphic function on Ω, namely the fixed set U1:=H(r,s) and the larger domain U2:=H^(r,s).

3.1L1step 2.1∎

By the definition in [L1], the existence of that common pair U1,U2 shows that Ω is not a domain of holomorphy.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-27Open item page →

An isolated puncture is removable in complex dimension at least two

Statement

Let m≥2, let Ω⊆Cm be a domain, let a∈Ω, and let f:Ω∖{a}→C be holomorphic. Then there exists a unique holomorphic F:Ω→C such that F=f on Ω∖{a}.

Facts & Assumptions

Given: A domain Ω⊆Cm with m≥2, a point a=(a1,a′)∈Ω, and a holomorphic function f:Ω∖{a}→C.

[L1]

Every point of an open subset of Cm has a polydisc neighborhood inside that open set (Balls, polydiscs and the distinguished boundary in Cm).

[L2]

A contour integral of a jointly continuous integrand that is holomorphic in the parameter variable defines a holomorphic function of that parameter (A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic).

[L3]

The one-variable Cauchy integral formula recovers a holomorphic function on a disc from any interior circle (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[L4]

A holomorphic function on a connected open set is determined by its values on a nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L5]

A separately holomorphic function that is locally bounded is jointly holomorphic (Locally bounded and separately holomorphic implies holomorphic).

Proof

technique · direct
1.1L1construct

By [L1], choose radii ρ1>ρ>0 and τ>0 with Δρ1(a1)×Δτ(a′)⊆Ω. For (z1,z′) with ∣z1−a1∣<ρ and ∣z′−a′∣<τ, define F(z1,z′):=12πi∫∣ζ−a1∣=ρf(ζ,z′)ζ−z1 dζ. When ∣ζ−a1∣=ρ and ∣z′−a′∣<τ, the point (ζ,z′) lies in Δρ1(a1)×Δτ(a′)∖{a}, so the integrand is well defined and continuous there.

2.1L2L5step 1.1algebra

Fix all variables except one. If the free variable is z1, the Cauchy kernel makes z1↦F(z1,z′) holomorphic on ∣z1−a1∣<ρ. If the free variable is one coordinate of z′, then [L2] applies to that single complex parameter. So F is separately holomorphic on Δρ(a1)×Δτ(a′). The same integral formula gives local bounds on compact subsets, so [L5] upgrades F to a jointly holomorphic function there.

2.2step 1.1L3

If z′≠a′, then the slice ζ↦f(ζ,z′) is holomorphic on the full disc ∣ζ−a1∣<ρ, because the deleted point a does not lie on that slice. Hence [L3] gives F(z1,z′)=f(z1,z′) for every ∣z1−a1∣<ρ.

3.1step 2.2L4

The set {(z1,z′)∈P:z′≠a′} is a nonempty open subset of P∖{a}, and step 2.2 shows that F and f agree there. Both are holomorphic on the connected punctured polydisc P∖{a}, so [L4] forces F=f on all of P∖{a}.

4.1step 2.1step 3.1L4∎

Thus F is a holomorphic extension of f across a on the neighborhood Δρ(a1)×Δτ(a′). Repeating the same construction at each puncture point gives a local extension, and uniqueness on overlaps again follows from [L4]. Therefore the local extensions glue to a unique holomorphic function on all of Ω.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-27Open item page →

Holomorphic functions of several variables have no isolated singularities

Statement

Let m≥2, let Ω⊆Cm be a domain, and let a∈Ω. A holomorphic function on Ω∖{a} cannot have a genuine isolated singularity at a: it always extends holomorphically across a.

Facts & Assumptions

Given: A domain Ω⊆Cm with m≥2, a point a∈Ω, and a holomorphic function on Ω∖{a}.

[L1]

In complex dimension at least two, a holomorphic function on a punctured domain extends uniquely across the puncture (An isolated puncture is removable in complex dimension at least two).

Proof

technique · direct
1.1L1

Apply [L1] to the punctured domain Ω∖{a}. It produces a holomorphic extension across a.

2.1step 1.1∎

So the deleted point cannot support a nonremovable isolated singularity.

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

A locally bounded punctured slice has a holomorphic parameter extension

Statement

Let m≥2, let ρ,R>0, let U:=Δρ(0)⊆Cm−1, and let f:U×{0<∣w∣<R}→C be holomorphic. Assume that for some 0<η<R the restriction of f to U×{0<∣w∣<η} is bounded. Define

F(z′):=12πi∫∣ζ∣=ηf(z′,ζ)ζ dζ.

Then F is holomorphic on U, and for every fixed z′∈U the one-variable slice w↦f(z′,w) extends holomorphically to ∣w∣<R with value F(z′) at w=0.

Facts & Assumptions

Given: A holomorphic function f on U×{0<∣w∣<R}, bounded on U×{0<∣w∣<η} for some 0<η<R.

[L1]

A punctured-disc holomorphic function extends across the centre exactly when it is bounded near that centre (Characterizations of removable singularities).

[L2]

A contour integral of a jointly continuous integrand that is holomorphic in the parameter variable defines a holomorphic function of that parameter (A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic).

[L3]

The one-variable Cauchy integral formula recovers a holomorphic function on a disc from a circle inside it (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[L4]

A separately holomorphic function that is locally bounded is jointly holomorphic (Locally bounded and separately holomorphic implies holomorphic).

Proof

technique · direct
1.1givenL1

Fix z′∈U. The slice w↦f(z′,w) is holomorphic on the punctured disc 0<∣w∣<R and bounded on 0<∣w∣<η. Therefore [L1] gives a holomorphic extension gz′ to the full disc ∣w∣<R.

1.2givenL2algebra

Fix one coordinate of z′ and hold the others fixed. For ∣ζ∣=η the integrand (z′,ζ)↦f(z′,ζ)/ζ is jointly continuous in that parameter and ζ, and for fixed ζ it is holomorphic in the chosen coordinate. So [L2] makes F separately holomorphic on U. The same circle formula gives local bounds on compact subsets of U, so F is locally bounded there.

2.1step 1.1L3

Applying [L3] to the holomorphic function gz′ on the circle ∣ζ∣=η gives gz′(0)=12πi∫∣ζ∣=ηf(z′,ζ)ζ dζ=F(z′). So F(z′) is exactly the removable value of the slice at w=0.

3.1step 2.1step 1.2L4∎

Step 2.1 identifies F(z′) with the extension value at w=0 for every z′. Step 1.2 makes F separately holomorphic and locally bounded, so [L4] upgrades it to a holomorphic function on U.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-27Open item page →

A locally bounded holomorphic function extends across a coordinate hyperplane

Statement

Let m≥2, let Ω⊆Cm be a domain, and let

H:=Ω∩{zm=0}.

If f:Ω∖H→C is holomorphic and locally bounded near H, then there exists a unique holomorphic F:Ω→C such that F=f on Ω∖H.

Facts & Assumptions

Given: A domain Ω⊆Cm, a holomorphic function f:Ω∖H→C, and local boundedness near the coordinate hyperplane H.

[L1]

A bounded punctured slice extends holomorphically, and the missing value depends holomorphically on the remaining parameters (A locally bounded punctured slice has a holomorphic parameter extension).

[L2]

A holomorphic function on a connected open set is determined by its values on a nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L3]

Holomorphic extension means agreement on some nonempty open overlap (Holomorphic extension and domains of holomorphy in several variables).

Proof

technique · direct
1.1givenL1

Let p=(p′,0)∈H. By local boundedness, choose a product neighborhood U×{∣w∣<R}⊆Ω of p on which f is bounded whenever 0<∣w∣<R, after translating coordinates so that pm=0. Applying [L1] on this product neighborhood gives a holomorphic function Fp:U×{∣w∣<R}→C extending f across the slice U×{0}.

2.1step 1.1L3

The functions Fp and f agree on the nonempty open overlap U×{0<∣w∣<R}, so each Fp is a local holomorphic extension in the sense of [L3].

3.1step 2.1L2

If two such neighborhoods overlap, their local extensions agree on the nonempty open subset of the overlap where w≠0, because both equal f there. The overlap is connected after shrinking if necessary, so [L2] makes the two local extensions equal on the whole overlap.

4.1step 3.1L2∎

The local extensions therefore glue to a single holomorphic function on Ω that agrees with f off H. Uniqueness follows from [L2], since two global extensions agree on the nonempty open set Ω∖H.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-27Open item page →

Separate holomorphy forces local boundedness on smaller polydiscs

Statement

Let m≥1, let R>0, and let

ΔRm:={z=(z1,…,zm)∈Cm:∣zj∣<R for every j}.

If f:ΔRm→C is separately holomorphic, then for every 0<r<R the function f is bounded on the closed polydisc Δ‾rm.

In particular, every separately holomorphic function on an open subset of Cm is locally bounded.

Facts & Assumptions

Given: A separately holomorphic function f on ΔRm and a radius 0<r<R.

[L1]

Separate holomorphy is the condition that each coordinate slice is one-variable holomorphic (Separately holomorphic functions).

[L3]

A separately holomorphic function that is locally bounded is jointly holomorphic (Locally bounded and separately holomorphic implies holomorphic).

[L4]

Jointly holomorphic functions are smooth, so their mixed derivatives are holomorphic (Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic).

[L5]

Cauchy estimates on a smaller polydisc bound Taylor coefficients by the supremum on that smaller distinguished boundary (Cauchy estimates for mixed derivatives on a polydisc).

[L6]

For a holomorphic one-variable function that is not identically zero on the connected component under consideration, the logarithm of the modulus is subharmonic (The logarithm of the modulus of a holomorphic function is subharmonic), and subharmonic means upper semicontinuous together with the disc submean inequality (Subharmonic functions on plane domains).

[L7]

Fatou's lemma controls the liminf of integrals of nonnegative measurable functions (Fatou's lemma), and monotone convergence controls increasing nonnegative boundary approximations (Monotone convergence for the integral).

[L9]

A holomorphic function on a connected open set is determined by its values on any nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L10]

Subharmonic functions satisfy harmonic comparison on discs; continuous circle data have harmonic Poisson extensions; and upper-semicontinuous circle data are Borel and bounded above (Subharmonicity is equivalent to harmonic comparison on compactly contained discs, The Poisson integral on the unit disc, The Poisson integral gives the unique continuous harmonic extension on the closed unit disc, Upper semicontinuous functions are Borel and their circle averages are defined).

Proof

technique · induction
1.1giveninduction

We prove a stronger local claim by induction on m: every separately holomorphic function on ΔRm is holomorphic on a neighborhood of each point of ΔRm. Once that is known, the displayed boundedness follows, because the compact set Δ‾rm is covered by finitely many such holomorphic neighborhoods and each holomorphic function is bounded on a smaller closed polydisc inside its neighborhood.

1.2L1baseih

Base case m=1: separate holomorphy is ordinary one-variable holomorphy by [L1], so the local claim and the boundedness statement are immediate. Assume now that the local claim is known in dimension m−1, and prove it in dimension m≥2.

1.3givenconstruct

Fix p∈ΔRm. Choose ρ>0 with 0<ρ<R and Δ‾2ρm(p)⊆ΔRm. After translating and rescaling each coordinate disc, it is enough to prove that a separately holomorphic function on Δ2m is holomorphic in a neighborhood of the origin. Write z=(z′,w) with z′∈Cm−1 and w∈C.

1.4L2inductionconstruct

Box claim. If a closed real box K=I1×⋯×Id⊆Rd is covered by countably many closed sets Fn, then some Fn contains a smaller closed real box with nondegenerate sides. We prove this by induction on d. For d=1 it is [L2]. Assume the claim in dimension d−1. Write K=I×K′. Enumerate the closed subboxes of K′ with rational endpoints in the coordinates of K′ as Q1,Q2,…. For each pair (n,j) let En,j:={x∈I:{x}×Qj⊆Fn}. Each En,j is closed. Fix x∈I. The sections Fn(x):={y∈K′:(x,y)∈Fn} are closed and cover K′, so the induction hypothesis in dimension d−1 gives some n such that Fn(x) contains a smaller closed box; shrinking slightly if needed, that box contains a rational-endpoint subbox Qj. Hence x∈En,j. So the countable family En,j covers I, and [L2] gives one pair (n,j) for which En,j contains a nondegenerate closed subinterval J. Then J×Qj⊆Fn, proving the claim.

1.5construct

Whenever 0≤d<1<η, one can choose radii d<s<r1<1<r2<η.

2.1L1step 1.2ih

For each positive integer B, define ΩB:={z′∈Δ‾1m−1:∣f(z′,w)∣≤B for every ∣w∣≤1}. For fixed w with ∣w∣≤1, the induction hypothesis applied to z′↦f(z′,w) makes that function holomorphic, hence continuous, on Δ2m−1. Therefore each set {z′:∣f(z′,w)∣≤B} is closed, and so every ΩB is closed. Also ⋃B≥1ΩB=Δ‾1m−1, because for fixed z′ the slice w↦f(z′,w) is holomorphic on Δ2 and therefore bounded on ∣w∣≤1.

3.1step 2.1step 1.4construct

Apply the box claim to the real box [−1/2,1/2]2m−2⊆Δ‾1m−1 and the closed cover (ΩB)B≥1. We obtain some B0 and a nondegenerate closed real box contained in ΩB0. Inside its relative interior choose a closed complex polydisc Δ‾2εm−1(a′) for some a′ and some ε>0. Its centre satisfies d:=max⁡1≤j<m∣aj′∣<1, and ∣f(z′,w)∣≤B0for z′∈Δ‾2εm−1(a′), ∣w∣≤1. Hence f is bounded on the product polydisc E:=Δ2εm−1(a′)×Δ1.

4.1L3step 3.1construct

By [L3], the separately holomorphic and bounded function f is jointly holomorphic on E. Put ζ=z′−a′ and retain the notation f(ζ,w) after this translation. The original first-variable domain contains the centred polydisc Δηm−1, where η:=2−d>1, while the original target z′=0 now has coordinate ζ=−a′. Thus f is separately holomorphic on Δηm−1×Δ2 and jointly holomorphic on Δ2εm−1×Δ1. Choose radii d<s<r1<1<r2<η, which is possible because d<1<η.

5.1L4L5L6step 1.2step 3.1step 4.1ih

For each multi-index α∈Nm−1, define cα(w):=1α! ∂ζαf(0,w)(∣w∣<1), using the jointly holomorphic function from step 4.1. By [L4], every cα is holomorphic on Δ1. For fixed w with ∣w∣<1, the induction hypothesis makes ζ↦f(ζ,w) holomorphic on Δηm−1, so these cα(w) are exactly its Taylor coefficients at 0. Since f is bounded by B0 on the larger product Δ2εm−1×Δ1, [L5] applied at the strictly smaller radius ε gives ∣cα(w)∣≤B0 ε−∣α∣(∣w∣<1). For each nonzero multi-index α with cα≢0, define uα(w):=∣α∣−1log⁡∣cα(w)∣. By [L6], each such uα is subharmonic on Δ1. If cα≡0, then the term cα(w)ζα vanishes identically and is already harmless for the later power-series tail estimate. The displayed estimate gives a uniform upper bound for the whole family (uα)α≠0, cα≢0.

6.1L5step 1.5step 5.1

Fix w∈Δ1. The Cauchy estimates [L5] applied to the holomorphic function ζ↦f(ζ,w) on Δηm−1, with the strictly smaller radius r2, show that ∣cα(w)∣≤M(w) r2−∣α∣ for some finite constant M(w) and every nonzero multi-index α. Therefore lim sup⁡∣α∣→∞cα≢0uα(w)≤−log⁡r2.

7.1L6step 5.1step 6.1

Let S:={α∈Nm−1∖{0}:cα≢0}. If S is finite, the required tail estimate is immediate. Otherwise enumerate it as (α(j))j≥1 with nondecreasing degrees and put vj=uα(j). By steps 5.1 and 6.1, the subharmonic functions vj have a common upper bound A on Δ1 and satisfy lim sup⁡jvj(w)≤C:=−log⁡r2 pointwise.

8.1L7L9L10step 7.1assume-contradischarge-contradiction

We claim that for every compact K⋐Δ1 and every δ>0, vj≤C+δ on K for all sufficiently large j. Otherwise choose jk↑∞ and qk∈K with vjk(qk)>C+δ, and pass to a subsequence with qk→q∈K. Choose t>0 with D(q,t)‾⊆Δ1, discard finitely many terms so qk∈D(q,t), and put Pk(θ):=P((qk−q)/t,eiθ). By the definition of S and [L9], no selected coefficient can vanish on a nonempty open subset of Δ1. More specifically for the boundary argument, vjk cannot be identically −∞ on the circle: if it were, every constant harmonic function −n would majorize its boundary values, so [L10] would give vjk(qk)≤−n for every n, contradicting the finite strict lower bound just chosen. For ζ on the circle define ϕk,n(ζ):=sup⁡η∈∂D(q,t)(vjk(η)−n∣ζ−η∣). Compactness and the common upper bound make each ϕk,n finite and continuous, and upper semicontinuity gives ϕk,n↓vjk pointwise. Harmonic comparison, their Poisson extensions, and monotone convergence in [L7] therefore give vjk(qk)≤12π∫02πPk(θ)vjk(q+teiθ) dθ. The kernels Pk tend uniformly to 1. The functions Pk(θ)(A−vjk(q+teiθ)) are nonnegative and measurable, so Fatou's lemma [L7] and the pointwise limsup bound make the lower limit of their normalized integrals at least A−C. Since each Pk has normalized integral 1, the preceding inequality gives lim sup⁡kvjk(qk)≤C, a contradiction.

9.1step 8.1algebra

Fix 0<σ<1. Apply step 8.1 to K=Δ‾σ and δ=log⁡(r2/r1)>0. For all sufficiently large j, vj(w)≤−log⁡r1(∣w∣≤σ), or equivalently ∣cα(j)(w)∣r1∣α(j)∣≤1.

10.1L8step 1.5step 9.1

Fix such a σ. If S is finite, then ∑αcα(w)ζα is a finite sum in ζ. Otherwise step 9.1 dominates its tail on Δ‾sm−1×Δ‾σ by the convergent product-geometric majorant ∑α(s/r1)∣α∣; the finitely many low-degree terms are harmless and the coefficients outside S vanish. Thus the series converges locally uniformly. Every partial sum is holomorphic, so [L8] gives a jointly holomorphic limit G(ζ,w) on Δsm−1×Δσ.

11.1step 4.1step 10.1L9

On the open set Δmin⁡(ε,s)m−1×Δσ, the Taylor expansion of the jointly holomorphic function from step 4.1 is exactly the series defining G. Thus G=f on that nonempty open set. For fixed w∈Δσ, both ζ↦G(ζ,w) and ζ↦f(ζ,w) are holomorphic on Δsm−1 and agree on a nonempty open subset, so [L9] gives equality on all of Δsm−1. Hence f=G on Δsm−1×Δσ, and f is jointly holomorphic there.

12.1step 1.1step 1.2step 1.3step 11.1discharge-induction∎

Because max⁡j∣−aj′∣=d<s and 0<σ, the translated coordinates of the original target, (−a′,0), lie in the product from step 11.1. Thus that step proves the required local holomorphicity at the original origin in dimension m. By the reductions in steps 1.1 and 1.3, every point of ΔRm has a holomorphic neighborhood. Therefore f is locally bounded on ΔRm, and in particular bounded on every smaller closed polydisc Δ‾rm. This closes the induction.

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

Separate holomorphy implies joint holomorphy in finite dimensions

Statement

Let m≥1, let U⊆Cm be open, and let f:U→C be separately holomorphic. Then f is holomorphic on U.

Facts & Assumptions

Given: An open set U⊆Cm and a separately holomorphic function f:U→C.

[L1]

Separate holomorphy means one-variable holomorphy on every coordinate slice (Separately holomorphic functions).

[L2]

A separately holomorphic function is locally bounded on every smaller polydisc (Separate holomorphy forces local boundedness on smaller polydiscs).

[L3]

A separately holomorphic function that is locally bounded is jointly holomorphic (Locally bounded and separately holomorphic implies holomorphic).

Proof

technique · direct
1.1givenL1L2

Fix p∈U. Because U is open, there is a polydisc neighborhood P⊆U of p. The restriction f∣P is still separately holomorphic by [L1], so [L2] makes it locally bounded near p.

2.1step 1.1L3∎

Applying [L3] to that same restriction shows that f is holomorphic on a neighborhood of p. As p was arbitrary, f is holomorphic on all of U.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-29Open item page →

Hartogs figures give local extension across polydisc shells

Statement

Fix m≥2, a point a=(a1,…,am)∈Cm, a polyradius ρ=(ρ1,…,ρm), and real numbers 0<r,s<1. Let S(a,ρ;r,s) be the subset of the polydisc Δρ(a) defined by

S(a,ρ;r,s):={z:∣z1−a1∣<ρ1, ∣zm−am∣<sρm, ∣zj−aj∣<ρj for 2≤j≤m−1}∪{z:rρ1<∣z1−a1∣<ρ1, ∣zm−am∣<ρm, ∣zj−aj∣<ρj for 2≤j≤m−1}.

Every holomorphic function on S(a,ρ;r,s) extends uniquely to a holomorphic function on the whole polydisc Δρ(a).

Facts & Assumptions

Given: A holomorphic function on the coordinate shell S(a,ρ;r,s).

[L1]

A contour integral of a jointly continuous integrand that is holomorphic in one chosen complex parameter defines a holomorphic function of that parameter (A contour integral of a jointly continuous, parameter-holomorphic integrand is holomorphic).

[L2]

Cauchy's integral formula on a circle recovers a holomorphic one-variable function from any smaller concentric circle (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[L3]

Holomorphic functions on a connected open set agree everywhere once they agree on one nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L4]

A separately holomorphic function that is locally bounded is jointly holomorphic (Locally bounded and separately holomorphic implies holomorphic).

[L5]

Polydiscs are products of coordinate discs (Balls, polydiscs and the distinguished boundary in Cm), and the two-variable Hartogs figure is the model set of The Hartogs figure H(r,s) and its bidisc hull.

Proof

technique · direct
1.1L5construct

By translating by a and scaling each coordinate by ρj−1, we may reduce to the case a=0 and ρj=1 for all j. Then the shell is exactly H(r,s)×Δ1m−2, with H(r,s) in the (z1,zm) variables and the middle variables passive.

2.1L5step 1.1construct

Fix ρ with r<ρ<1. On the domain Dρ:={z:∣z1∣<ρ, ∣zj∣<1 for 2≤j≤m} define [construct] Fρ(z):=12πi∫∣ζ∣=ρf(ζ,z2,…,zm)ζ−z1 dζ. Because ∣ζ∣=ρ>r and ∣zj∣<1 for j≥2, every point (ζ,z2,…,zm) lies in the shell from step 1.1, so the integral is well defined.

3.1L1step 2.1

Fix all variables except one coordinate of z∈Dρ. For the z1 variable, the integrand in step 2.1 is jointly continuous on the contour times {∣z1∣<ρ} and holomorphic in z1, so [L1] makes z1↦Fρ(z) holomorphic. For any coordinate zk with 2≤k≤m, the denominator is constant and the slice zk↦f(ζ,z2,…,zm) is holomorphic on the unit disc because f is holomorphic on the shell. Another use of [L1] makes zk↦Fρ(z) holomorphic. Therefore Fρ is separately holomorphic on Dρ.

3.2L2step 2.1

If ∣zm∣<s, then for fixed z2,…,zm−1 the slice z1↦f(z1,z2,…,zm) is holomorphic on the full unit disc. Applying [L2] on the circle ∣ζ∣=ρ gives Fρ(z)=f(z)(∣z1∣<ρ, ∣zm∣<s, ∣zj∣<1 for 2≤j≤m−1). So Fρ agrees with f on a nonempty open subset of the shell.

4.1L4step 2.1step 3.1

Let K⊆Dρ be compact. Choose δ>0 so that ∣z1∣≤ρ−δ on K. The set {(ζ,z2,…,zm):∣ζ∣=ρ, z∈K} is a compact subset of the shell, so ∣f∣ has a finite bound MK there. The contour in step 2.1 has length 2πρ, and ∣ζ−z1∣≥δ on that contour for z∈K, hence ∣Fρ(z)∣≤12π∫∣ζ∣=ρMK∣ζ−z1∣ ∣dζ∣≤ρMKδ(z∈K). Thus Fρ is locally bounded on Dρ, so [L4] upgrades step 3.1 to joint holomorphicity on Dρ.

5.1L3step 4.1step 3.2

If r<ρ1<ρ2<1, then both Fρ1 and Fρ2 are holomorphic on Dρ1 by step 4.1, and step 3.2 shows that they agree on the nonempty open subset of Dρ1 where ∣zm∣<s. Therefore [L3] gives Fρ1=Fρ2 on all of Dρ1.

6.1L3step 3.2step 4.1step 5.1∎

For each point z of the full polydisc from step 1.1, choose any ρ with max⁡{r,∣z1∣}<ρ<1 and set F(z):=Fρ(z). Step 5.1 makes this definition independent of ρ, and step 4.1 shows that F is holomorphic near each point. For fixed ρ, the open set S(0,1;r,s)∩Dρ is connected: its central part ∣zm∣<s meets its annular part r<∣z1∣<ρ, and each part is connected. On this set Fρ and f are holomorphic and agree on the nonempty central part by step 3.2, so [L3] gives Fρ=f throughout it. Every shell point lies in one such Dρ, hence F extends f on the entire shell. If G is another holomorphic extension to the full polydisc, then F and G agree with f on the same nonempty open subset where ∣zm∣<s, so [L3] forces F=G. Thus the extension is unique.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Local Hartogs extensions propagate along chains and glue uniquely

Statement

Let Ω⊆Cm be open, let G⊆Ω be a connected open set, and let U1,…,UN⊆Ω be domains with Uj∩G≠∅ for every j. Assume that for each j and every g∈O(Uj∩G) there is Eg∈O(Uj) satisfying Eg=g on all of Uj∩G, and that after reordering every connected component of

Uj∩(G∪U1∪⋯∪Uj−1)(2≤j≤N).

meets G.

Then every holomorphic function on G extends uniquely to a holomorphic function on G∪U1∪⋯∪UN.

Facts & Assumptions

Given: A connected open set G, open sets U1,…,UN, and the local extension property stated above.

[L1]

The local-extension hypothesis here explicitly requires agreement on the whole set Uj∩G, which is stronger than agreement on one open overlap in the general extension convention (Holomorphic extension and domains of holomorphy in several variables).

[L2]

Coordinate shell neighborhoods are one class of open sets with the stated local extension property (Hartogs figures give local extension across polydisc shells).

[L3]

Holomorphic functions on a connected open set agree everywhere once they agree on one nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

Proof

technique · direct
1.1L1given

Let f∈O(G). By the explicit hypothesis for j=1, there is F1∈O(U1) with F1=f on all of U1∩G. Hence f and F1 glue to a holomorphic function on G∪U1.

2.1L3step 1.1

Assume inductively that we have already obtained a holomorphic extension Fj−1 on G∪U1∪⋯∪Uj−1. By hypothesis, the restriction of Fj−1 to Uj∩G extends holomorphically to some Ej on Uj. Let C be a connected component of Uj∩(G∪U1∪⋯∪Uj−1). The hypothesis makes C∩G nonempty, and since both C and G are open, C∩G is a nonempty open subset of C. On that open set, Ej and Fj−1 both agree with f. Therefore [L3] makes them equal on the whole connected set C. This holds for every overlap component, so Ej and Fj−1 glue to a holomorphic function Fj on G∪U1∪⋯∪Uj.

3.1step 2.1L2L3discharge-construct∎

Repeating step 2.1 for j=2,…,N yields a holomorphic extension on the whole union G∪U1∪⋯∪UN. Uniqueness at each stage follows from [L3], so the final extension is unique. The shell lemma [L2] identifies the geometric neighborhoods used later.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-09-29Open item page →

Hartogs extension across a connected compact hole with a finite shell cover

Statement

Let m≥2, let Ω⊆Cm be a domain, and let K⋐Ω be compact with Ω∖K connected. Assume that K admits a finite shell cover: there are open polydiscs P1,…,PN⊆Ω covering K such that

  1. for each j, the punctured set Pj∩(Ω∖K) is connected and contains a coordinate shell of the type treated in Hartogs figures give local extension across polydisc shells whose hull is Pj;
  2. after reordering, every connected component of Pj∩((Ω∖K)∪P1∪⋯∪Pj−1) has nonempty intersection with Ω∖K for every j≥2.

Then every holomorphic function on Ω∖K extends uniquely to a holomorphic function on Ω.

Facts & Assumptions

Given: A domain Ω, a compact set K⋐Ω, connected complement Ω∖K, and a finite shell cover P1,…,PN as in the Statement.

[L1]

Each coordinate shell extends holomorphically to its hull polydisc (Hartogs figures give local extension across polydisc shells).

[L2]

Local extension neighborhoods propagate along finite chains and glue uniquely (Local Hartogs extensions propagate along chains and glue uniquely).

[L3]

Holomorphic functions on connected open sets are determined by agreement on one nonempty open subset (A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically).

[L4]

Holomorphic extension is the overlap-agreement notion fixed on this page (Holomorphic extension and domains of holomorphy in several variables).

Proof

technique · direct
1.1L1L2L3given

Put G:=Ω∖K and let f∈O(G). For each j, choose the shell Sj⊆Pj∩G from assumption 1. Given any g∈O(Pj∩G), [L1] extends g∣Sj to a holomorphic Eg on the hull Pj. The functions Eg and g agree on the nonempty open set Sj inside the connected open set Pj∩G; by [L3] they agree on all of Pj∩G. This is the full-overlap local extension property required by [L2], for every g, not only for f. Each Pj∩G is nonempty because it contains Sj, and assumption 2 is exactly the componentwise overlap condition of [L2]. Thus (Pj) satisfies every hypothesis of [L2].

2.1step 1.1L2

Applying [L2] gives a holomorphic extension of f from G to G∪P1∪⋯∪PN. Because the polydiscs cover K, this union is all of Ω.

3.1L3L4step 2.1∎

Uniqueness follows from [L3]: two extensions to Ω agree on the nonempty open subset Ω∖K, so they agree on all of the connected domain Ω. The overlap language in [L4] is exactly the one used in step 1.1.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

FALSE: every holomorphic function on a punctured several-variable domain is unbounded near the puncture

Statement

False claim: if m≥2 and f is holomorphic on a punctured neighborhood of 0∈Cm, then f must be unbounded near 0.

Facts & Assumptions

Given: The bounded coordinate function f(z)=z1 on Δ1m∖{0} with m≥2.

[L1]

A holomorphic function on a punctured several-variable domain extends holomorphically across the missing point (An isolated puncture is removable in complex dimension at least two).

Refutation

technique · direct
1.1givenalgebra

The function f(z)=z1 is holomorphic on Δ1m∖{0} and satisfies ∣f(z)∣≤1 there, so it is bounded near the puncture.

2.1step 1.1L1∎

Step 1.1 already contradicts the displayed claim, and [L1] explains why no singularity is hiding here: the function extends holomorphically across 0 as the same coordinate function.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

FALSE: isolated singularities in several variables can be poles or essential

Statement

False claim: in complex dimension at least two, an isolated singularity can still be removable, a pole, or essential just as in one variable.

Facts & Assumptions

Given: Complex dimension m≥2.

[L1]

In one variable every isolated singularity is exactly one of the removable, pole, or essential cases (Every isolated singularity is removable, a pole, or essential).

[L2]

In several variables with m≥2, an isolated deleted point is always removable (Holomorphic functions of several variables have no isolated singularities).

Refutation

technique · direct
1.1L1

The one-variable trichotomy of [L1] distinguishes three genuinely different behaviors at a puncture.

2.1L2step 1.1∎

In several variables with m≥2, [L2] collapses that trichotomy at an isolated point: the only possible behavior is removability. So poles and essential singularities do not occur at isolated deleted points.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

FALSE: every domain in C^2 is a domain of holomorphy

Statement

False claim: every domain in C2 is a domain of holomorphy.

Facts & Assumptions

Given: Real numbers 0<r,s<1 and the Hartogs figure domain Ω:=H(r,s).

[L1]

A domain that contains a Hartogs figure but not its hull is not a domain of holomorphy (A domain containing a Hartogs figure but not its hull is not a domain of holomorphy).

Refutation

technique · direct
1.1givenalgebra

The domain Ω=H(r,s) contains the Hartogs figure H(r,s) itself, while its hull is the full bidisc H^(r,s), which strictly contains Ω.

2.1step 1.1L1∎

Therefore [L1] applies directly and shows that Ω is not a domain of holomorphy, refuting the claim.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

FALSE: separate holomorphy can fail to imply local boundedness

Statement

False claim: a separately holomorphic function on a finite-dimensional polydisc need not be locally bounded.

Facts & Assumptions

Given: A separately holomorphic function on a polydisc.

[L1]

Separate holomorphy forces boundedness on every smaller closed polydisc (Separate holomorphy forces local boundedness on smaller polydiscs).

Refutation

technique · direct
1.1given

Let f be separately holomorphic on a polydisc.

2.1step 1.1L1∎

The conclusion of [L1] applies directly to f, so f is locally bounded. This contradicts the displayed claim.

5 · Examples, counterexamples and false statements

None yet.

Sources