Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-29
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.

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.

Depends on

Used by

Dependency tree · two levels

43 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