CorollaryStatement: Literature-sourcedProof: 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 coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique

Statement

Let $m \geq 1$ , $a \in C^{m}$ and let $r$ be a polyradius. Suppose $c, c^{'} : N^{m} \to C$ both satisfy a bound $∣ c_{α} ∣ \leq M \prod_{k < m} r_{k}^{- α_{k}}$ and $∣ c_{α}^{'} ∣ \leq M^{'} \prod_{k < m} r_{k}^{- α_{k}}$ , and suppose

$\sum_{α} c_{α} (z - a)^{α} = \sum_{α} c_{α}^{'} (z - a)^{α} for every z \in Δ_{r} (a) .$

Then $c_{α} = c_{α}^{'}$ for every multi-index $α$ . In particular a function has at most one such power-series representation about a given centre, and its coefficients are $\partial_{z}^{α} f (a) / α!$ .

Facts & Assumptions

Given: Coefficient families $c, c^{'}$ with the stated bounds whose sums agree on $Δ_{r} (a)$ .

[L1]

Under a bound $∣ c_{α} ∣ \leq M \prod_{k < m} r_{k}^{- α_{k}}$ the series converges absolutely on $Δ_{r} (a)$ , its sum is holomorphic there, every iterated complex partial derivative of the sum exists, and $\partial_{z}^{α} (sum) (a) = α! c_{α}$ (An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise).

[L2]

A holomorphic function is locally the sum of an absolutely convergent power series whose coefficients are $\partial_{z}^{α} f (a) / α!$ , and every iterated complex partial derivative is holomorphic (Holomorphic functions of several variables are smooth and their complex derivatives are holomorphic).

[L3]

Multi-indexed power series and their absolute convergence are those of Multi-indexed power series in $C^{m}$ and their absolute convergence; $α! = \prod_{k < m} α_{k}!$ ( $C^{k}$ maps and multi-index derivative notation in Euclidean space) and $α! \neq 0$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L4]

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

Proof

technique · direct

1.1

Let $f$ be the common sum on $Δ_{r} (a)$ . By [L1] applied to $c$ , the function $f$ is holomorphic on $Δ_{r} (a)$ , every $\partial_{z}^{α} f$ exists there, and $\partial_{z}^{α} f (a) = α! c_{α}$ .

givenL1L3L4

1.2

By [L1] applied to $c^{'}$ , the same function $f$ satisfies $\partial_{z}^{α} f (a) = α! c_{α}^{'}$ ; the derivatives are those of the single function $f$ and so do not depend on which series it is written as.

givenL1L3L4

2.1

Comparing steps 1.1 and 1.2 gives $α! c_{α} = α! c_{α}^{'}$ , and $α! \neq 0$ by [L3], so $c_{α} = c_{α}^{'}$ for every $α$ .

step 1.1step 1.2L3

3.1

Consequently a holomorphic $f$ has at most one power-series representation about $a$ subject to such a bound, and by [L2] the one it has is the derivative series $\sum_{α} \partial_{z}^{α} f (a) (z - a)^{α} / α!$ ; this is what licenses the definite article in "the coefficients of $f$ at $a$ ".

step 2.1L2∎

Depends on

Used by

Dependency tree · two levels

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