TheoremStatement: AI-adaptedProof: AI-adaptedprecheck 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 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} ι (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 $ι (n) (x - c)^{n - 1}$ for $n \geq 1$ (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (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.1givenchoose

Fix $x_{0}$ with $∣ x_{0} - c ∣ < R$ and choose a closed interval $J$ containing both $c$ and $x_{0}$ strictly inside the radius.

1.2L1L2L4

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

2.1step 1.2L3

The sequence $p_{N} (c)$ converges to $a_{0}$ , since it equals $a_{0}$ for every $N \geq 1$ . 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}^{'})$ .

3.1step 2.1L1∎

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.

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources