Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27
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.

Separate holomorphy forces local boundedness on smaller polydiscs

Statement

Let m1, let R>0, and let

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

If f:ΔRmC 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.1

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.

giveninduction
1.2

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 m1, and prove it in dimension m2.

L1baseih
1.3

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 zCm1 and wC.

givenconstruct
1.4

Box claim. If a closed real box K=I1××IdRd 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 d1. 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:={xI:{x}×QjFn}. Each En,j is closed. Fix xI. The sections Fn(x):={yK:(x,y)Fn} are closed and cover K, so the induction hypothesis in dimension d1 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 xEn,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×QjFn, proving the claim.

L2inductionconstruct
1.5

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

construct
2.1

For each positive integer B, define ΩB:={zΔ1m1:f(z,w)B for every w1}. For fixed w with w1, the induction hypothesis applied to zf(z,w) makes that function holomorphic, hence continuous, on Δ2m1. Therefore each set {z:f(z,w)B} is closed, and so every ΩB is closed. Also B1ΩB=Δ1m1, because for fixed z the slice wf(z,w) is holomorphic on Δ2 and therefore bounded on w1.

L1step 1.2ih
3.1

Apply the box claim to the real box [1/2,1/2]2m2Δ1m1 and the closed cover (ΩB)B1. We obtain some B0 and a nondegenerate closed real box contained in ΩB0. Inside its relative interior choose a closed complex polydisc Δ2εm1(a) for some a and some ε>0. Its centre satisfies d:=max1j<maj<1, and f(z,w)B0for zΔ2εm1(a), w1. Hence f is bounded on the product polydisc E:=Δ2εm1(a)×Δ1.

step 2.1step 1.4construct
4.1

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

L3step 3.1construct
5.1

For each multi-index αNm1, 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 Δηm1, so these cα(w) are exactly its Taylor coefficients at 0. Since f is bounded by B0 on the larger product Δ2εm1×Δ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):=α1logcα(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.

L4L5L6step 1.2step 3.1step 4.1ih
6.1

Fix wΔ1. The Cauchy estimates [L5] applied to the holomorphic function ζf(ζ,w) on Δηm1, 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)logr2.

L5step 1.5step 5.1
7.1

Let S:={αNm1{0}:cα≢0}. If S is finite, the required tail estimate is immediate. Otherwise enumerate it as (α(j))j1 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 supjvj(w)C:=logr2 pointwise.

L6step 5.1step 6.1
8.1

We claim that for every compact KΔ1 and every δ>0, vjC+δ on K for all sufficiently large j. Otherwise choose jk and qkK with vjk(qk)>C+δ, and pass to a subsequence with qkqK. Choose t>0 with D(q,t)Δ1, discard finitely many terms so qkD(q,t), and put Pk(θ):=P((qkq)/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,nvjk 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(θ)(Avjk(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 AC. Since each Pk has normalized integral 1, the preceding inequality gives lim supkvjk(qk)C, a contradiction.

L7L9L10step 7.1assume-contradischarge-contradiction
9.1

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

step 8.1algebra
10.1

Fix such a σ. If S is finite, then αcα(w)ζα is a finite sum in ζ. Otherwise step 9.1 dominates its tail on Δsm1×Δσ 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 Δsm1×Δσ.

L8step 1.5step 9.1
11.1

On the open set Δmin(ε,s)m1×Δσ, 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 Δsm1 and agree on a nonempty open subset, so [L9] gives equality on all of Δsm1. Hence f=G on Δsm1×Δσ, and f is jointly holomorphic there.

step 4.1step 10.1L9
12.1

Because maxjaj=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.

step 1.1step 1.2step 1.3step 11.1discharge-induction

Depends on

Used by

Dependency tree · two levels

75 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