Theorem 8.2 — Abel's limit theorem

Proved

Rudin.ch08_abel

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

analysisseries

If $\sum c_n$ converges to $C$ and $f(x) = \sum c_n x^n$ for $|x| < 1$ , then $f(x) \to C$ as $x \to 1^-$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch03_series

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.2 (Abel's theorem): if `∑ cₙ` converges to `C` and `f x = ∑ cₙ xⁿ` for
`|x| < 1`, then `f x → C` as `x → 1⁻`. -/
theorem ch08_abel (c : ℕ → ℝ) (C : ℝ) (hC : SeriesConvergesTo c C) (f : ℝ → ℝ)
    (hf : ∀ x : ℝ, |x| < 1 → SeriesConvergesTo (fun n => c n * x ^ n) (f x)) :
    Tendsto f (𝓝[<] (1 : ℝ)) (𝓝 C) := by sorry

end Rudin

Source

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

Read-back

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

Let $c : \mathbb{N}\to\mathbb{R}$ and $C \in \mathbb{R}$ with the partial sums $\sum_{i<n} c_i$ converging to $C$ . Let $f : \mathbb{R}\to\mathbb{R}$ be such that for every real $x$ with $|x| < 1$ the partial sums of $\sum_n c_n x^n$ converge to $f(x)$ . Then

f(x) \longrightarrow C \quad \text{as } x \to 1^{-},

the limit being along the filter of left neighbourhoods of $1$ in $\mathbb{R}$ (so through points $x < 1$ , which for $x$ near $1$ lie in $(-1,1)$ where $f$ is pinned down by the hypothesis).

Nothing is assumed about $f$ outside $(-1,1)$ , and no absolute convergence is required.

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