LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 separately holomorphic function on a polydisc is Lipschitz on every smaller polydisc

Statement

Let $m \geq 1$ , let $a \in C^{m}$ , let $ρ$ be a polyradius, let $f : Δ_{ρ} (a) \to C$ be separately holomorphic (Separately holomorphic functions) with $∣ f ∣ \leq M$ throughout $Δ_{ρ} (a)$ , and let $0 < θ < 1$ . Then for all $z, w \in {\overline{Δ}}_{θ ρ} (a)$

$∣ f (w) - f (z) ∣ \leq \frac{M}{1 - θ} \sum_{k < m} \frac{∣ w_{k} - z_{k} ∣}{ρ_{k}} \leq \frac{M}{1 - θ} (\sum_{k < m} \frac{1}{ρ_{k}}) ∥ w - z ∥ .$

In particular $f$ is Lipschitz, hence continuous, on ${\overline{Δ}}_{θ ρ} (a)$ . No continuity of $f$ in the remaining variables is assumed at any point of the argument.

Facts & Assumptions

Given: A separately holomorphic $f$ on $Δ_{ρ} (a)$ with $∣ f ∣ \leq M$ there, and $0 < θ < 1$ ; $C^{m}$ is read through Complex $m$ -space and its real coordinate dictionary.

[L1]

$f$ is separately holomorphic when for every point of the open set and every $k < m$ the $k$ th slice is holomorphic on the open set of $ζ$ for which the point lies in the domain (Separately holomorphic functions).

[L2]

$Δ_{r} (a)$ , ${\overline{Δ}}_{r} (a)$ and $Γ_{r} (a)$ are defined coordinatewise by $∣ z_{k} - a_{k} ∣ < r_{k}$ , $\leq r_{k}$ and $= r_{k}$ , and polydiscs are convex (Balls, polydiscs and the distinguished boundary in $C^{m}$ , A convex subset of $R^{m}$ contains every line segment between two of its points).

[L3]

For $g$ holomorphic on $D (a^{'}, R)$ , $0 < r^{'} < R$ and $∣ g ∣ \leq K$ on the circle $∣ ζ - a^{'} ∣ = r^{'}$ , one has $∣ g^{(n)} (a^{'}) ∣ \leq n! K / r^{' n}$ (Cauchy's inequalities bound every derivative by a boundary bound on a compactly contained circle).

[L4]

For an open convex $V \subseteq C$ , a holomorphic $g$ on $V$ and $z^{'}, w^{'} \in V$ , $g (w^{'}) - g (z^{'}) = (w^{'} - z^{'}) \int_{0}^{1} g^{'} (z^{'} + t (w^{'} - z^{'})) d t$ (On a convex open set the difference quotient is an average of the derivative along the segment).

[L5]

For an integrable $F : [a^{'}, b^{'}] \to R^{n}$ with $a^{'} \leq b^{'}$ , $∥ \int_{a^{'}}^{b^{'}} F ∥_{2} \leq \int_{a^{'}}^{b^{'}} ∥ F ∥_{2}$ (For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable); vector-valued integrals are componentwise and real-linear (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral); and $\int_{a^{'}}^{b^{'}} h \leq \int_{a^{'}}^{b^{'}} H$ when $h \leq H$ pointwise (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L6]

A holomorphic $g = u + i v$ on an open subset of $C$ has $(u, v)$ of class $C^{k}$ for every natural $k$ , hence smooth (Holomorphic functions are real analytic and smooth in their two real coordinates), and every holomorphic function has complex derivatives of every natural order (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle); in particular $g^{'}$ is holomorphic and therefore continuous (Complex differentiability at a point implies continuity there).

[L7]

Finite sums are additive, scale and telescope (Laws of finite sums and finite products, Finite sums and finite products, by recursion).

[L8]

$∣ z w ∣ = ∣ z ∣ ∣ w ∣$ and $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive), and $B (x, s) = {y : d (x, y) < s}$ (Open ball, closed ball and sphere in a metric space).

[L9]

If a property holds at $0$ and passes from $k$ to $k + 1$ , it holds for every natural number (The principle of mathematical induction).

[L10]

A nonempty set of reals bounded below has a greatest lower bound (Every nonempty set bounded below has an infimum, Greatest lower bound (infimum)).

Proof

technique · direct

1.1

Fix $z, w \in {\overline{Δ}}_{θ ρ} (a)$ and define points $v^{(0)}, \dots, v^{(m)}$ by $v^{(0)} = z$ and, for $k < m$ , letting $v^{(k + 1)}$ agree with $v^{(k)}$ except that its $k$ th coordinate is $w_{k}$ ; this is a finite recursion and $v^{(m)} = w$ . Every coordinate of every $v^{(k)}$ is a coordinate of $z$ or of $w$ , so $∣ v_{j}^{(k)} - a_{j} ∣ \leq θ ρ_{j}$ for every $j < m$ and each $v^{(k)}$ lies in ${\overline{Δ}}_{θ ρ} (a) \subseteq Δ_{ρ} (a)$ by [L2].

givenL2L9

2.1

By [L7] the difference telescopes: $f (w) - f (z) = \sum_{k < m} (f (v^{(k + 1)}) - f (v^{(k)}))$ .

step 1.1L7

2.2

Fix $k < m$ and let $g_{k} (ξ)$ be the value of $f$ at the point agreeing with $v^{(k)}$ except in its $k$ th coordinate, which is $ξ$ . By step 1.1 and [L2] that point lies in $Δ_{ρ} (a)$ whenever $∣ ξ - a_{k} ∣ < ρ_{k}$ , so [L1] makes $g_{k}$ holomorphic on the disc $D (a_{k}, ρ_{k})$ , and $∣ g_{k} ∣ \leq M$ there.

step 1.1L1L2

3.1

Let $∣ ξ - a_{k} ∣ \leq θ ρ_{k}$ and let $0 < s < (1 - θ) ρ_{k}$ . For $∣ ζ - ξ ∣ < (1 - θ) ρ_{k}$ one has $∣ ζ - a_{k} ∣ < ρ_{k}$ by [L8], so $g_{k}$ is holomorphic on $D (ξ, (1 - θ) ρ_{k})$ and bounded by $M$ on the circle $∣ ζ - ξ ∣ = s$ ; [L3] with $n = 1$ gives $∣ g_{k}^{'} (ξ) ∣ \leq M / s$ . The set of such $s$ is nonempty and the bound holds for each, so taking the infimum over $s \in (0, (1 - θ) ρ_{k})$ by [L10] gives $∣ g_{k}^{'} (ξ) ∣ \leq M / ((1 - θ) ρ_{k})$ .

step 2.2L3L8L10

4.1

The disc $D (a_{k}, ρ_{k})$ is convex by [L2] and [L8], and $z_{k}, w_{k}$ lie in the closed disc of radius $θ ρ_{k}$ about $a_{k}$ by step 1.1, so the whole segment between them satisfies $∣ ξ - a_{k} ∣ \leq θ ρ_{k}$ by [L8]. By [L4], [L6] and [L5], $∣ g_{k} (w_{k}) - g_{k} (z_{k}) ∣ \leq ∣ w_{k} - z_{k} ∣ \int_{0}^{1} ∣ g_{k}^{'} (z_{k} + t (w_{k} - z_{k})) ∣ d t \leq ∣ w_{k} - z_{k} ∣ \cdot \frac{M}{(1 - θ) ρ_{k}}$ , using step 3.1 on the segment.

step 1.1step 3.1L2L4L5L6L8

5.1

Since $f (v^{(k + 1)}) - f (v^{(k)}) = g_{k} (w_{k}) - g_{k} (z_{k})$ by the definition of $g_{k}$ in step 2.2, summing step 4.1 over $k < m$ and using step 2.1 and [L7] gives $∣ f (w) - f (z) ∣ \leq \frac{M}{1 - θ} \sum_{k < m} ∣ w_{k} - z_{k} ∣ / ρ_{k}$ ; each $∣ w_{k} - z_{k} ∣ \leq ∥ w - z ∥$ by the dictionary, which yields the second displayed bound and makes $f$ Lipschitz on ${\overline{Δ}}_{θ ρ} (a)$ . Only the slices of $f$ and the uniform bound $M$ were used, never continuity of $f$ in the remaining variables.

step 2.1step 2.2step 4.1L7L8∎

Depends on

Used by

Dependency tree · two levels

105 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

J. Lebl, Tasty Bits of Several Complex Variables, §1.2 (standard reference, not scraped)
H. P. Boas, Lecture Notes on Multidimensional Complex Analysis, Ch. 2 (standard reference, not scraped)