TheoremStatement: Literature-sourcedProof: 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.

Osgood's lemma: continuous and separately holomorphic implies holomorphic

Statement

Let $m \geq 1$ , let $U \subseteq C^{m}$ be open and let $f : U \to C$ be continuous and separately holomorphic (Separately holomorphic functions). Then $f$ is holomorphic on $U$ (Holomorphic functions on an open subset of $C^{m}$ ).

Consequently, for a continuous $f$ on an open $U$ the following three conditions are equivalent: $f$ is holomorphic; $f$ is separately holomorphic; every point of $U$ has a polydisc neighbourhood on which $f$ is the sum of an absolutely convergent multi-indexed power series.

Facts & Assumptions

Given: An open $U \subseteq C^{m}$ and a continuous separately holomorphic $f : U \to C$ ; $C^{m}$ is read through Complex $m$ -space and its real coordinate dictionary.

[L1]

For $f$ continuous and separately holomorphic on $Δ_{ρ} (a)$ and a polyradius $r$ with $r_{k} < ρ_{k}$ , the iterated-integral coefficients satisfy $∣ c_{α} ∣ \leq M \prod_{k < m} r_{k}^{- α_{k}}$ with $M = \sup_{Γ_{r} (a)} ∣ f ∣$ , and $f (z) = \sum_{α} c_{α} (z - a)^{α}$ on $Δ_{r} (a)$ , absolutely and uniformly on every ${\overline{Δ}}_{θ r} (a)$ with $θ < 1$ (A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc).

[L2]

If $∣ c_{α} ∣ \leq M \prod_{k < m} r_{k}^{- α_{k}}$ for every $α$ , then $\sum_{α} c_{α} (z - a)^{α}$ converges absolutely on $Δ_{r} (a)$ and its sum is holomorphic there (An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise).

[L3]

A holomorphic function of several variables is continuous and separately holomorphic (A holomorphic function of several variables is continuous and separately holomorphic).

[L4]

Holomorphic on $U$ means complex differentiable at every point of $U$ (Holomorphic functions on an open subset of $C^{m}$ ), and separate holomorphy is a condition on the slices through each point (Separately holomorphic functions).

[L5]

$Δ_{r} (a)$ is defined coordinatewise by $∣ z_{k} - a_{k} ∣ < r_{k}$ (Balls, polydiscs and the distinguished boundary in $C^{m}$ ), and a multi-indexed power series and its absolute convergence are those of Multi-indexed power series in $C^{m}$ and their absolute convergence.

[L6]

A set is open exactly when each of its points admits a ball inside it, and $B (x, ε) = {y : d (x, y) < ε}$ (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).

[L7]

$∣ 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).

Proof

technique · direct

1.1

Fix $a \in U$ . By [L6] there is $ε > 0$ with $B (a, ε) \subseteq U$ ; put $ρ_{k} = ε / (2 \sqrt{m})$ for every $k < m$ . If $z \in Δ_{ρ} (a)$ then $∥ z - a ∥^{2} = \sum_{k < m} ∣ z_{k} - a_{k} ∣^{2} < m ρ_{0}^{2} = ε^{2} / 4$ by [L5] and the dictionary, so $Δ_{ρ} (a) \subseteq B (a, ε) \subseteq U$ .

givenL5L6L7

1.2

The restriction of $f$ to $Δ_{ρ} (a)$ is continuous, and it is separately holomorphic there: for $b \in Δ_{ρ} (a)$ and $k < m$ the slice domain inside $Δ_{ρ} (a)$ is an open subset of the slice domain inside $U$ , on which the slice is holomorphic by hypothesis, and a restriction of a holomorphic function of one variable to an open subset is holomorphic.

givenL4L5

2.1

Put $r_{k} = ρ_{k} / 2$ , so $r_{k} < ρ_{k}$ . By [L1] applied on $Δ_{ρ} (a)$ there are coefficients $c_{α}$ with $∣ c_{α} ∣ \leq M \prod_{k < m} r_{k}^{- α_{k}}$ and $f (z) = \sum_{α} c_{α} (z - a)^{α}$ for every $z \in Δ_{r} (a)$ .

step 1.1step 1.2L1L5

3.1

By [L2] the sum of that series is holomorphic on $Δ_{r} (a)$ ; by step 2.1 it is $f$ there, so $f$ is complex differentiable at every point of $Δ_{r} (a)$ , in particular at $a$ . Since $a \in U$ was arbitrary, [L4] makes $f$ holomorphic on $U$ .

step 2.1L2L4

4.1

For the equivalence, let $f$ be continuous on the open $U$ . If $f$ is holomorphic then it is separately holomorphic by [L3]; if it is separately holomorphic then step 2.1 gives the local power-series representation and step 3.1 gives holomorphy; and if it is locally such a sum then [L2] makes it holomorphic on a polydisc about each point, hence on $U$ by [L4]. So the three conditions are equivalent.

step 2.1step 3.1L2L3L4∎

Depends on

Used by

Dependency tree · two levels

73 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

H. P. Boas, Lecture Notes on Multidimensional Complex Analysis, Ch. 2 (standard reference, not scraped)
M. Jabbari, Notes for Analysis and Geometry of Several Complex Variables, §3.1 (standard reference, not scraped)