CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

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 power-series sum is infinitely differentiable inside its radius and satisfies $a_n=f^{(n)}(c)/\iota(n!)$ at its centre

Statement

Let $f(x)=\sum_{n\ge0}a_n(x-c)^n$ have positive or infinite radius $R$ . Define $f^{(0)}:=f$ and $f^{(m+1)}:=(f^{(m)})'$ . Then every derivative exists on $|x-c|<R$ , and for each $m\in\mathbb N$ ,

$f^{(m)}(x)=\sum_{j=0}^{\infty}\iota\!\left((m+j)^{\underline m}\right)a_{m+j}(x-c)^j.$

In particular,

$f^{(m)}(c)=\iota(m!)a_m,\qquad a_m=\frac{f^{(m)}(c)}{\iota(m!)}.$

Facts & Assumptions

Given: A power-series sum $f$ of radius $R>0$ and the recursively defined derivatives $f^{(m)}$ .

[L1]

A power series may be differentiated term by term throughout its open radius, and its first derived series has the same radius (Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius).

[L2]

Falling factorials satisfy $n^{\underline0}=1$ and $n^{\underline{k+1}}=n^{\underline k}(n-k)$ for all natural $n,k$ , with truncated difference $n-k$ , and $n^{\underline n}=n!\ne0$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $\mathbb{N}$ ); the canonical embedding into $\mathbb R$ is multiplicative and injective (Laws of finite sums and products in $\mathbb{N}$ , and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$ ).

[L3]

The induction principle on $\mathbb N$ (The principle of mathematical induction).

Proof

technique · induction

1.1

For $m=0$ , the formula reads $f(x)=\sum_{j\ge0}\iota(j^{\underline0})a_j(x-c)^j=\sum_{j\ge0}a_j(x-c)^j$ , so the claim holds.

basegivenL2

1.2

Fix $m$ and assume the displayed formula for $f^{(m)}$ , with radius $R$ .

2.1

By [L1], differentiate the series in step 1.2 term by term. Reindexing $j+1$ as $j$ gives $f^{(m+1)}(x)=\sum_{j\ge0}\iota(j+1)\iota((m+j+1)^{\underline m})a_{m+j+1}(x-c)^j$ .

step 1.2L1

3.1

The falling-factorial recursion with $n=m+j+1$ and $k=m$ gives $(m+j+1)^{\underline{m+1}}=(m+j+1)^{\underline m}(j+1)$ . Since $\iota$ preserves products, step 2.1 is precisely the asserted formula with $m+1$ in place of $m$ .

step 2.1L2algebra

4.1

By [L3], the derivative formula holds for every $m$ . At each induction step [L1] also preserves the radius $R$ , so every derived series has radius $R$ .

step 1.1step 3.1L1L3discharge-induction

5.1

At $x=c$ , every term with $j\ge1$ vanishes and the $j=0$ term is $\iota(m^{\underline m})a_m=\iota(m!)a_m$ ; since $m!\ne0$ , division gives the coefficient formula.

step 4.1L2discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 88 results over 18 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

Power series, Encyclopedia of Mathematics (standard reference, not scraped)
E. Randles, Supplementary Notes for Real Analysis (standard reference, not scraped)

A power-series sum is infinitely differentiable inside its radius and satisfies an=f(n)(c)/ι(n!)a_n=f^{(n)}(c)/\iota(n!)an​=f(n)(c)/ι(n!) at its centre