Theorem 8.5 — identity theorem for power series

Proved

Rudin.ch08_identity_theorem

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

analysisseries

If $\sum a_n x^n$ and $\sum b_n x^n$ converge on $(-R,R)$ and their sums agree on a set $E$ having a limit point in $(-R,R)$ , then $a_n = b_n$ for all $n$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch03_series

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.5: if two power series converge on `(-R, R)` and their sums agree on a set
which has a limit point in `(-R, R)`, then the two series have the same coefficients. -/
theorem ch08_identity_theorem (a b : ℕ → ℝ) (R : ℝ) (hR : 0 < R) (f g : ℝ → ℝ)
    (hf : ∀ x : ℝ, |x| < R → SeriesConvergesTo (fun n => a n * x ^ n) (f x))
    (hg : ∀ x : ℝ, |x| < R → SeriesConvergesTo (fun n => b n * x ^ n) (g x))
    (E : Set ℝ) (hE : E ⊆ Set.Ioo (-R) R) (hagree : ∀ x ∈ E, f x = g x)
    (x₀ : ℝ) (hx₀ : x₀ ∈ Set.Ioo (-R) R) (hlim : x₀ ∈ closure (E \ {x₀})) :
    ∀ n, a n = b n := by sorry

end Rudin

Source

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

Read-back

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

Let $a, b : \mathbb{N}\to\mathbb{R}$ be two coefficient sequences, let $R > 0$ , and let $f, g : \mathbb{R}\to\mathbb{R}$ be such that for every $x$ with $|x| < R$ the partial sums of $\sum_n a_n x^n$ converge to $f(x)$ and those of $\sum_n b_n x^n$ converge to $g(x)$ . Let $E \subseteq (-R,R)$ be a set on which $f$ and $g$ agree: $f(x) = g(x)$ for all $x \in E$ . Suppose further that there is a point $x_0 \in (-R,R)$ lying in the closure of $E \setminus \{x_0\}$ (i.e. $x_0$ is a limit point of $E$ , whether or not $x_0 \in E$ ).

Then $a_n = b_n$ for every $n \in \mathbb{N}$ .

The conclusion is equality of all coefficients, not merely of the sum functions. Convergence is assumed on the full open interval $(-R,R)$ for both series.

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