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

The iterated Cauchy integral formula on a polydisc

Statement

Fix $m \geq 1$ , a point $a \in C^{m}$ and a polyradius $ρ$ . Let $f : Δ_{ρ} (a) \to C$ be continuous and separately holomorphic (Separately holomorphic functions), let $r$ be a polyradius with $r_{k} < ρ_{k}$ for every $k < m$ , and let $C_{k} (t) = a_{k} + r_{k} \exp (i t)$ on $[0, 2 π]$ . Then for every $z \in Δ_{r} (a)$

$f (z) = \frac{1}{(2 π i)^{m}} \int_{C_{0}} ⁣ \dots ⁣ \int_{C_{m - 1}} \frac{f (ζ_{0}, \dots, ζ_{m - 1})}{\prod_{k < m} (ζ_{k} - z_{k})} d ζ_{m - 1} \dots d ζ_{0} .$

The right-hand side is an iterated integral: the innermost integral is taken over $ζ_{m - 1}$ with $ζ_{0}, \dots, ζ_{m - 2}$ held fixed, then over $ζ_{m - 2}$ , and so on. Each successive integrand is continuous on the circle it is integrated over, so each of the $m$ integrals exists. No integral over the distinguished boundary is formed and the order of integration is never interchanged.

Facts & Assumptions

Given: $m \geq 1$ , $a \in C^{m}$ , polyradii $ρ$ and $r$ with $r_{k} < ρ_{k}$ , a continuous separately holomorphic $f : Δ_{ρ} (a) \to C$ , the circles $C_{k}$ , and $z \in Δ_{r} (a)$ ; $C^{m}$ is read through Complex $m$ -space and its real coordinate dictionary.

[L1]

$Δ_{r} (a)$ , ${\overline{Δ}}_{r} (a)$ and $Γ_{r} (a)$ are defined coordinatewise by $∣ z_{k} - a_{k} ∣ < r_{k}$ , $\leq r_{k}$ and $= r_{k}$ (Balls, polydiscs and the distinguished boundary in $C^{m}$ ).

[L2]

$f$ is separately holomorphic when for every $b \in U$ and $k < m$ the slice $ζ \mapsto f (b_{0}, \dots, b_{k - 1}, ζ, b_{k + 1}, \dots, b_{m - 1})$ is holomorphic on the open set of $ζ$ for which the point lies in $U$ (Separately holomorphic functions).

[L3]

If $f$ is holomorphic on $D (a^{'}, R)$ , $0 < r^{'} < R$ , $∣ z^{'} - a^{'} ∣ < r^{'}$ and $γ (t) = a^{'} + r^{'} \exp (i t)$ on $[0, 2 π]$ , then $f (z^{'}) = (2 π i)^{- 1} \int_{γ} f (ζ) (ζ - z^{'})^{- 1} d ζ$ (Cauchy's integral formula on a circle compactly contained in a disc of holomorphy).

[L4]

For a rectifiable contour and an integrand continuous on its trace, the complex line integral exists (Continuous integrands have complex and absolute line integrals along every rectifiable path, The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral).

[L5]

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

[L6]

For $a^{'} \in C$ , $r^{'} > 0$ and $k \in Z$ , the contour $a^{'} + r^{'} \exp (i k t)$ on $[0, 2 π]$ is a closed complex contour whose trace for $k \neq 0$ is ${∣ \cdot - a^{'} ∣ = r^{'}}$ (A circle traversed $k$ times has winding number $k$ inside and $0$ outside).

[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).

[L8]

Nonvanishing quotients of functions complex differentiable at a point are complex differentiable there (Linearity, product, reciprocal, and quotient rules for complex derivatives), such functions are continuous (Complex differentiability at a point implies continuity there), and composites of continuous maps are continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous).

Proof

technique · direct

1.1

By [L6] each $C_{k}$ is a closed complex contour with trace the circle ${∣ ζ - a_{k} ∣ = r_{k}}$ . If $∣ ζ_{j} - a_{j} ∣ = r_{j}$ for $j < p$ and $∣ z_{j} - a_{j} ∣ < r_{j}$ for $j \geq p$ , then $∣ ζ_{j} - a_{j} ∣ < ρ_{j}$ and $∣ z_{j} - a_{j} ∣ < ρ_{j}$ by the hypothesis $r_{j} < ρ_{j}$ , so every such mixed point lies in $Δ_{ρ} (a)$ by [L1].

givenL1L6

1.2

For the fixed point $z$ , define $H_{m} (ζ_{0}, \dots, ζ_{m - 1}; z) : = f (ζ_{0}, \dots, ζ_{m - 1})$ . Then, for $p = m - 1, m - 2, \dots, 0$ , define $H_{p} (ζ_{0}, \dots, ζ_{p - 1}; z)$ by $H_{p} : = \frac{1}{2 π i} \int_{C_{p}} \frac{H_{p + 1} (ζ_{0}, \dots, ζ_{p - 1}, ζ_{p}; z)}{ζ_{p} - z_{p}} d ζ_{p},$ whenever the integrand is continuous on $C_{p}$ . By construction $H_{0} (; z)$ is exactly the iterated integral in the statement, divided by $(2 π i)^{m}$ .

given

2.1

Claim, proved by induction on $q = m - p$ using [L5]: for every $p$ with $0 \leq p \leq m$ the quantity $H_{p}$ is defined and $H_{p} (ζ_{0}, \dots, ζ_{p - 1}; z) = f (ζ_{0}, \dots, ζ_{p - 1}, z_{p}, \dots, z_{m - 1})$ . For $q = 0$ , that is $p = m$ , this is the definition of $H_{m}$ .

step 1.1step 1.2L5

2.2

The slice $ξ \mapsto f (ζ_{0}, \dots, ζ_{p - 1}, ξ, z_{p + 1}, \dots, z_{m - 1})$ is holomorphic on the disc $∣ ξ - a_{p} ∣ < ρ_{p}$ : by step 1.1 the corresponding point lies in $Δ_{ρ} (a)$ for every such $ξ$ , and by [L1] and [L2] that disc is exactly the slice domain, on which separate holomorphy makes the slice holomorphic.

step 1.1L1L2

3.1

Assume the claim for $p + 1$ . Fix $ζ_{0}, \dots, ζ_{p - 1}$ on their circles. By the assumption, $H_{p + 1} (ζ_{0}, \dots, ζ_{p - 1}, ζ_{p}; z) = f (ζ_{0}, \dots, ζ_{p}, z_{p + 1}, \dots, z_{m - 1})$ , which by step 1.1 is a continuous function of $ζ_{p}$ on the circle $∣ ζ_{p} - a_{p} ∣ = r_{p}$ ; dividing by $ζ_{p} - z_{p}$ , which is nonzero there because $∣ z_{p} - a_{p} ∣ < r_{p}$ by [L1] and [L7], leaves a continuous integrand by [L8], so the integral defining $H_{p}$ exists by [L4].

step 1.1step 2.1L1L4L7L8

4.1

Applying [L3] to the slice of step 2.2, with $R = ρ_{p}$ , $r^{'} = r_{p}$ and $z^{'} = z_{p}$ , gives $f (ζ_{0}, \dots, ζ_{p - 1}, z_{p}, z_{p + 1}, \dots, z_{m - 1}) = \frac{1}{2 π i} \int_{C_{p}} \frac{f (ζ_{0}, \dots, ζ_{p - 1}, ζ_{p}, z_{p + 1}, \dots)}{ζ_{p} - z_{p}} d ζ_{p}$ , which by step 3.1 is $H_{p} (ζ_{0}, \dots, ζ_{p - 1}; z)$ . This is the claim for $p$ , so the induction of step 2.1 closes.

step 3.1step 2.2L3

5.1

Taking $p = 0$ in step 2.1 gives $H_{0} (; z) = f (z)$ , and step 1.2 identifies $H_{0} (; z)$ with the iterated integral divided by $(2 π i)^{m}$ ; every one of the $m$ integrals exists by step 3.1. Since $z \in Δ_{r} (a)$ was arbitrary, the formula holds throughout $Δ_{r} (a)$ .

step 1.2step 2.1step 3.1step 4.1∎

Depends on

Used by

Dependency tree · two levels

80 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)
M. Jabbari, Notes for Analysis and Geometry of Several Complex Variables, §3.1 (standard reference, not scraped)