CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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 complex power-series sum has complex derivatives of every order, obtained by repeated termwise differentiation

Statement

If $f (z) = \sum_{n \geq 0} c_{n} (z - a)^{n}$ has radius $R$ , then for every $k \in N$ and $∣ z - a ∣ < R$ , $f^{(k)} (z) = \sum_{n \geq k} \frac{n!}{(n - k)!} c_{n} (z - a)^{n - k} .$ Every derived series has radius $R$ .

Facts & Assumptions

Given: A complex power series $f$ of radius $R$ .

[L1]

A complex power series may be differentiated term by term inside its radius (Inside its disc of convergence a complex power series is holomorphic and may be differentiated term by term).

[L2]

A complex power series $\sum_{n \geq 0} c_{n} (z - a)^{n}$ , its formal derivative $\sum_{n \geq 0} (n + 1) c_{n + 1} (z - a)^{n}$ , and its zero-constant-term formal antiderivative $\sum_{n \geq 0} c_{n} (z - a)^{n + 1} / (n + 1)$ have the same radius of convergence (A complex power series, its formal derivative, and its zero-constant-term formal antiderivative have the same radius).

[L3]

Falling factorials satisfy $n^{\underline{k}} = n! / (n - k)!$ when $k \leq n$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

Proof

technique · induction

1.1

For $k = 0$ , the displayed formula is the original series because $n! / (n - 0)! = 1$ .

baseL3

1.2

Assume the formula holds for $k$ , with its series having radius $R$ . [L2] is stated for one series and its formal derivative, so it is applied once at this induction step, to the $k$ th series: its formal derivative again has radius $R$ . That is exactly what the induction needs, and no claim about "every successive derivative" is taken from [L2] at once. Then [L1] differentiates termwise and changes the coefficient $n! / (n - k)!$ into $n! / (n - k - 1)!$ for $n \geq k + 1$ .

ihL1L2L3

2.1

Thus the formula holds for $k + 1$ , and induction gives it for every $k$ . The cases $k > n$ contribute no term and $k = 0$ was the base case.

step 1.1step 1.2discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 61 results over 15 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

E. Stein and R. Shakarchi, Complex Analysis, Ch. 1, §2.3 (standard reference, not scraped)