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

Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius

Statement

Let

$f(x)=\sum_{n=0}^{\infty}a_n(x-c)^n$

have radius $R$ . For every $x$ with $|x-c|<R$ , the function $f$ is differentiable at $x$ (The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set) and

$f'(x)=\sum_{n=0}^{\infty}\iota(n+1)a_{n+1}(x-c)^n.$

The differentiated series has the same radius $R$ .

Facts & Assumptions

Given: A real power series of radius $R$ with polynomial partial sums $p_N(x):=\sum_{n<N}a_n(x-c)^n$ .

[L1]

The formal derivative series has radius $R$ (A power series, its formal derivative, and its zero-constant-term formal antiderivative have the same radius of convergence).

[L2]

A power series converges uniformly on every closed interval strictly inside its radius (A power series converges absolutely and uniformly on every closed interval strictly inside its interval of convergence).

[L3]

If continuously differentiable functions converge at one point of a closed interval and their derivatives converge uniformly, then the functions converge uniformly to a differentiable function whose derivative is the derivative limit (If continuously differentiable functions converge at one point and their derivatives converge uniformly on a closed interval, then the functions converge uniformly to a differentiable function whose derivative is the derivative limit).

[L4]

The derivative of $(x-c)^n$ is $0$ for $n=0$ and $\iota(n)(x-c)^{n-1}$ for $n\ge1$ (For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term and the algebra of derivatives cited there).

Proof

technique · direct

1.1

Fix $x_0$ with $|x_0-c|<R$ and choose a closed interval $J$ containing both $c$ and $x_0$ strictly inside the radius.

givenchoose

1.2

Each $p_N$ is continuously differentiable on $J$ , and [L4] gives $p_N'(x)=\sum_{n<N-1}\iota(n+1)a_{n+1}(x-c)^n$ . The derivative partial sums converge uniformly on $J$ by [L1] and [L2].

L1L2L4

2.1

The sequence $p_N(c)$ converges to $a_0$ , since it equals $a_0$ for every $N\ge1$ . Thus [L3] applies and says that the uniform limit of $(p_N)$ on $J$ is differentiable with derivative equal to the uniform limit of $(p_N')$ .

step 1.2L3

3.1

The uniform limit of $(p_N)$ is $f$ , and the limit of $(p_N')$ is the displayed differentiated series. Hence the formula holds at $x_0$ ; since $x_0$ was arbitrary it holds throughout $|x-c|<R$ , and [L1] supplies the equality of radii.

step 2.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

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

MIT 18.100C, Lecture 11: Power Series (standard reference, not scraped)
Power series, Encyclopedia of Mathematics (standard reference, not scraped)
E. Randles, Supplementary Notes for Real Analysis (standard reference, not scraped)