LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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 Cauchy kernel expands as an absolutely and uniformly convergent multi-indexed geometric series

Statement

Fix $m \geq 1$ , a point $a \in C^{m}$ , a polyradius $r$ and a real $θ$ with $0 \leq θ < 1$ . For $ζ \in Γ_{r} (a)$ and $z \in {\overline{Δ}}_{θ r} (a)$ , that is $∣ ζ_{k} - a_{k} ∣ = r_{k}$ and $∣ z_{k} - a_{k} ∣ \leq θ r_{k}$ for every $k < m$ ,

$\prod_{k < m} \frac{1}{ζ_{k} - z_{k}} = \sum_{α} (z - a)^{α} \prod_{k < m} (ζ_{k} - a_{k})^{- α_{k} - 1},$

the multi-indexed series converging absolutely (Multi-indexed power series in $C^{m}$ and their absolute convergence). Each term is dominated by

$M_{α} : = \prod_{k < m} \frac{θ^{α_{k}}}{r_{k}}, \sum_{α} M_{α} = \prod_{k < m} \frac{1}{r_{k} (1 - θ)},$

independently of $ζ$ and $z$ , so the convergence is absolute and uniform in the pair $(ζ, z)$ over $Γ_{r} (a) \times {\overline{Δ}}_{θ r} (a)$ .

Facts & Assumptions

Given: $m \geq 1$ , $a \in C^{m}$ , a polyradius $r$ , a real $θ$ with $0 \leq θ < 1$ , and points $ζ \in Γ_{r} (a)$ , $z \in {\overline{Δ}}_{θ r} (a)$ ; $C^{m}$ is read through Complex $m$ -space and its real coordinate dictionary.

[L1]

A multi-indexed series converges absolutely at $z$ when the series along one, equivalently every, bijection $σ : N \to N^{m}$ converges absolutely, its sum is then independent of $σ$ , and its box partial sums over $B_{N} = {α : α_{k} \leq N}$ converge to that sum (Multi-indexed power series in $C^{m}$ and their absolute convergence).

[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}$ (Balls, polydiscs and the distinguished boundary in $C^{m}$ ).

[L3]

A complex series converges absolutely when the real series of moduli converges (Complex series, absolute convergence, complex power series, and radius of convergence); an absolutely convergent complex series converges and every rearrangement has the same sum (Every absolutely convergent complex series converges, and rearrangements preserve its sum).

[L4]

If $∣ f_{n} (x) ∣ \leq M_{n}$ on a set $X$ with $\sum M_{n}$ convergent, then $\sum f_{n} (x)$ converges absolutely for every $x$ and its partial sums converge uniformly on $X$ (Weierstrass M-test for complex-valued function series, Uniform convergence and the uniformly Cauchy condition for complex-valued functions, with the componentwise dictionary).

[L5]

Negative integer powers are defined exactly for nonzero complex bases (Integer powers in the complex field).

[L6]

For real $r^{'}$ with $∣ r^{'} ∣ < 1$ , $\sum_{k} r^{' k}$ converges with sum $1 / (1 - r^{'})$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges), and $(r^{' k})$ is null (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

[L7]

A nonnegative series converges exactly when its partial sums are bounded above (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum).

[L8]

Sums over finite index sets in a commutative monoid are well posed; finite Cartesian-box sums factor by repeated finite Fubini, and distributivity in $C$ permits the finite sum/product factorisations used below (A finite sum in a commutative monoid indexed by an arbitrary finite set, Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule, $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

[L9]

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

For $k < m$ put $u_{k} = (z_{k} - a_{k}) / (ζ_{k} - a_{k})$ , legitimate by [L2] and [L5] since $∣ ζ_{k} - a_{k} ∣ = r_{k} > 0$ ; then $∣ u_{k} ∣ \leq θ < 1$ by [L2] and [L9], and $ζ_{k} - z_{k} = (ζ_{k} - a_{k}) (1 - u_{k})$ with $∣ 1 - u_{k} ∣ \geq 1 - θ > 0$ by [L9].

givenL2L5L9

1.2

Each term satisfies $∣ (z - a)^{α} \prod_{k < m} (ζ_{k} - a_{k})^{- α_{k} - 1} ∣ = \prod_{k < m} (∣ z_{k} - a_{k} ∣^{α_{k}} r_{k}^{- α_{k} - 1}) \leq \prod_{k < m} θ^{α_{k}} / r_{k} = M_{α}$ , by [L2], [L8] and [L9].

givenL2L8L9

2.1

For $N \in N$ the box sum of the majorants factors as $\sum_{α \in B_{N}} M_{α} = \prod_{k < m} (r_{k}^{- 1} \sum_{j \leq N} θ^{j})$ by [L8], which is at most $\prod_{k < m} (r_{k} (1 - θ))^{- 1}$ by [L6]. Every finite subset of $N^{m}$ lies in some $B_{N}$ , so along any bijection $σ$ the partial sums of $\sum_{n} M_{σ (n)}$ are bounded by that number, and [L7] makes the series convergent; letting $N \to \infty$ in the factored identity and using [L6] gives $\sum_{α} M_{α} = \prod_{k < m} (r_{k} (1 - θ))^{- 1}$ .

step 1.2L6L7L8

2.2

The box partial sum factors: by [L8], $\sum_{α \in B_{N}} (z - a)^{α} \prod_{k < m} (ζ_{k} - a_{k})^{- α_{k} - 1} = \prod_{k < m} (\frac{1}{ζ_{k} - a_{k}} \sum_{j \leq N} u_{k}^{j}) = \prod_{k < m} \frac{1 - u_{k}^{N + 1}}{(ζ_{k} - a_{k}) (1 - u_{k})}$ , the last equality by the finite geometric identity $(1 - u) \sum_{j \leq N} u^{j} = 1 - u^{N + 1}$ and step 1.1.

step 1.1L5L8algebra

3.1

By step 1.2 and step 2.1 the hypotheses of [L4] hold with the constants $M_{α}$ on the set $Γ_{r} (a) \times {\overline{Δ}}_{θ r} (a)$ , so the series converges absolutely at every such pair and its partial sums along $σ$ converge uniformly there; by [L1] and [L3] the sum is independent of $σ$ and the box partial sums converge to it.

step 1.2step 2.1L1L3L4

3.2

By step 1.1 the target value is $\prod_{k < m} ((ζ_{k} - a_{k}) (1 - u_{k}))^{- 1}$ , so the difference from the box sum of step 2.2 has modulus at most $\prod_{k < m} (r_{k} (1 - θ))^{- 1} \cdot ∣ 1 - \prod_{k < m} (1 - u_{k}^{N + 1}) ∣$ by [L9]; since $∣ u_{k}^{N + 1} ∣ \leq θ^{N + 1}$ , [L9] and [L8] bound the second factor by $(1 + θ^{N + 1})^{m} - 1$ , which tends to $0$ as $N \to \infty$ by [L6].

step 1.1step 2.2L6L8L9

4.1

Hence the box partial sums converge to $\prod_{k < m} (ζ_{k} - z_{k})^{- 1}$ , and by step 3.1 they also converge to the sum of the series; the two limits agree, which is the displayed expansion, with the majorant and the uniformity already recorded in steps 1.2 and 3.1.

step 3.1step 3.2∎

Depends on

Used by

A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc Theorem

Dependency tree · two levels

90 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)