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 , let , and let
If is separately holomorphic, then for every the function is bounded on the closed polydisc .
In particular, every separately holomorphic function on an open subset of is locally bounded.
Facts & Assumptions
Given: A separately holomorphic function on and a radius .
Separate holomorphy is the condition that each coordinate slice is one-variable holomorphic (Separately holomorphic functions).
A countable closed cover of a nondegenerate closed interval contains one member that contains a nondegenerate closed subinterval (Baire category inside a closed bounded interval: if with is covered by a sequence of closed sets, then one of them contains a nondegenerate closed subinterval of ; no choice principle is used).
A separately holomorphic function that is locally bounded is jointly holomorphic (Locally bounded and separately holomorphic implies holomorphic).
Jointly holomorphic functions are smooth, so their mixed derivatives are holomorphic (Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic).
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).
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).
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).
A locally uniform limit of holomorphic functions is holomorphic (Locally uniform limits of holomorphic functions are holomorphic, with locally uniform convergence of all derivatives).
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).
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
We prove a stronger local claim by induction on : every separately holomorphic function on is holomorphic on a neighborhood of each point of . Once that is known, the displayed boundedness follows, because the compact set is covered by finitely many such holomorphic neighborhoods and each holomorphic function is bounded on a smaller closed polydisc inside its neighborhood.
Base case : 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 , and prove it in dimension .
Fix . Choose with and . After translating and rescaling each coordinate disc, it is enough to prove that a separately holomorphic function on is holomorphic in a neighborhood of the origin. Write with and .
Box claim. If a closed real box is covered by countably many closed sets , then some contains a smaller closed real box with nondegenerate sides. We prove this by induction on . For it is [L2]. Assume the claim in dimension . Write . Enumerate the closed subboxes of with rational endpoints in the coordinates of as . For each pair let Each is closed. Fix . The sections are closed and cover , so the induction hypothesis in dimension gives some such that contains a smaller closed box; shrinking slightly if needed, that box contains a rational-endpoint subbox . Hence . So the countable family covers , and [L2] gives one pair for which contains a nondegenerate closed subinterval . Then , proving the claim.
Whenever , one can choose radii .
For each positive integer , define For fixed with , the induction hypothesis applied to makes that function holomorphic, hence continuous, on . Therefore each set is closed, and so every is closed. Also , because for fixed the slice is holomorphic on and therefore bounded on .
Apply the box claim to the real box and the closed cover . We obtain some and a nondegenerate closed real box contained in . Inside its relative interior choose a closed complex polydisc for some and some . Its centre satisfies and Hence is bounded on the product polydisc .
By [L3], the separately holomorphic and bounded function is jointly holomorphic on . Put and retain the notation after this translation. The original first-variable domain contains the centred polydisc , where , while the original target now has coordinate . Thus is separately holomorphic on and jointly holomorphic on . Choose radii , which is possible because .
For each multi-index , define using the jointly holomorphic function from step 4.1. By [L4], every is holomorphic on . For fixed with , the induction hypothesis makes holomorphic on , so these are exactly its Taylor coefficients at . Since is bounded by on the larger product , [L5] applied at the strictly smaller radius gives For each nonzero multi-index with , define . By [L6], each such is subharmonic on . If , then the term 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 .
Fix . The Cauchy estimates [L5] applied to the holomorphic function on , with the strictly smaller radius , show that for some finite constant and every nonzero multi-index . Therefore
Let If is finite, the required tail estimate is immediate. Otherwise enumerate it as with nondecreasing degrees and put . By steps 5.1 and 6.1, the subharmonic functions have a common upper bound on and satisfy pointwise.
We claim that for every compact and every , on for all sufficiently large . Otherwise choose and with , and pass to a subsequence with . Choose with , discard finitely many terms so , and put . By the definition of and [L9], no selected coefficient can vanish on a nonempty open subset of . More specifically for the boundary argument, cannot be identically on the circle: if it were, every constant harmonic function would majorize its boundary values, so [L10] would give for every , contradicting the finite strict lower bound just chosen. For on the circle define Compactness and the common upper bound make each finite and continuous, and upper semicontinuity gives pointwise. Harmonic comparison, their Poisson extensions, and monotone convergence in [L7] therefore give The kernels tend uniformly to . The functions are nonnegative and measurable, so Fatou's lemma [L7] and the pointwise limsup bound make the lower limit of their normalized integrals at least . Since each has normalized integral , the preceding inequality gives , a contradiction.
Fix . Apply step 8.1 to and . For all sufficiently large , or equivalently .
Fix such a . If is finite, then is a finite sum in . Otherwise step 9.1 dominates its tail on by the convergent product-geometric majorant ; the finitely many low-degree terms are harmless and the coefficients outside vanish. Thus the series converges locally uniformly. Every partial sum is holomorphic, so [L8] gives a jointly holomorphic limit on .
On the open set , the Taylor expansion of the jointly holomorphic function from step 4.1 is exactly the series defining . Thus on that nonempty open set. For fixed , both and are holomorphic on and agree on a nonempty open subset, so [L9] gives equality on all of . Hence on , and is jointly holomorphic there.
Because and , the translated coordinates of the original target, , lie in the product from step 11.1. Thus that step proves the required local holomorphicity at the original origin in dimension . By the reductions in steps 1.1 and 1.3, every point of has a holomorphic neighborhood. Therefore is locally bounded on , and in particular bounded on every smaller closed polydisc . This closes the induction.
Depends on
- Separately holomorphic functions
- Baire category inside a closed bounded interval: if $[a,b]$ with $a < b$ is covered by a sequence of closed sets, then one of them contains a nondegenerate closed subinterval of $[a,b]$; no choice principle is used
- Locally bounded and separately holomorphic implies holomorphic
- Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic
- Cauchy estimates for mixed derivatives on a polydisc
- The logarithm of the modulus of a holomorphic function is subharmonic
- Subharmonic functions on plane domains
- Upper semicontinuous functions are Borel and their circle averages are defined
- 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
- Monotone convergence for the integral
- Fatou's lemma
- Locally uniform limits of holomorphic functions are holomorphic, with locally uniform convergence of all derivatives
- A holomorphic function vanishing on a nonempty open subset of a domain vanishes identically
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
- Paul Garrett, Hartogs' Theorem: separate analyticity implies joint (standard reference, not scraped)
- J. Lebl, Tasty Bits of Several Complex Variables, §1.2 and Appendix E (standard reference, not scraped)