Theorem 8.1 — term-by-term differentiation of power series

Proved

Rudin.ch08_power_series_derivative

by Lucas · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisseries

If $\sum c_n x^n$ converges for $|x| < R$ with sum $f(x)$ , and $g(x)$ is the sum of the differentiated series $\sum n c_n x^{n-1}$ there, then $f$ is differentiable on $(-R,R)$ with $f' = g$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch03_series

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.1: if the power series `∑ cₙ xⁿ` converges for `|x| < R` and `f` is its
sum, then `f` is differentiable on `(-R, R)` and its derivative is obtained by term-by-term
differentiation. -/
theorem ch08_power_series_derivative (c : ℕ → ℝ) (R : ℝ) (hR : 0 < R)
    (hconv : ∀ x : ℝ, |x| < R → SeriesConverges (fun n => c n * x ^ n))
    (f : ℝ → ℝ) (hf : ∀ x : ℝ, |x| < R → SeriesConvergesTo (fun n => c n * x ^ n) (f x))
    (g : ℝ → ℝ) (hg : ∀ x : ℝ, |x| < R →
      SeriesConvergesTo (fun n => (n : ℝ) * c n * x ^ (n - 1)) (g x)) :
    ∀ x : ℝ, |x| < R → HasDerivAt f (g x) x := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8, p. 173, Theorem 8.1

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $c : \mathbb{N}\to\mathbb{R}$ , let $R > 0$ , and let $f, g : \mathbb{R}\to\mathbb{R}$ . Assume:

for every real $x$ with $|x| < R$ , the series $\sum_n c_n x^n$ converges (its partial sums have a real limit);
for every such $x$ , the partial sums of $\sum_n c_n x^n$ converge to $f(x)$ ;
for every such $x$ , the partial sums of the term-by-term differentiated series, whose $n$ -th term is $n\,c_n\,x^{\,n-1}$ , converge to $g(x)$ . Here $n-1$ is truncated natural subtraction, so the $n=0$ term is $0 \cdot c_0 \cdot x^0 = 0$ .

Then for every $x$ with $|x| < R$ , $f$ is differentiable at $x$ with derivative exactly $g(x)$ .

$f$ and $g$ are arbitrary functions on all of $\mathbb{R}$ constrained only on the interval $(-R,R)$ by the hypotheses; nothing is asserted outside it, nor about uniform convergence or about $|x| = R$ .

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph