Theorem 7.26 — Weierstrass approximation theorem

Proved

Rudin.ch07_weierstrass_approximation

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

analysisapproximation

If $f$ is a continuous complex function on $[a,b]$ , there is a sequence of polynomials $P_n$ with $P_n \to f$ uniformly on $[a,b]$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch07_families

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 7.26 (Weierstrass approximation theorem): every continuous complex function
on `[a, b]` is the uniform limit on `[a, b]` of a sequence of polynomials. -/
theorem ch07_weierstrass_approximation (a b : ℝ) (hab : a ≤ b) (f : ℝ → ℂ)
    (hf : ContinuousOn f (Set.Icc a b)) :
    ∃ P : ℕ → Polynomial ℂ,
      TendstoUniformlyOn (fun n (x : ℝ) => (P n).eval (x : ℂ)) f atTop (Set.Icc a b) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 7, p. 159, Theorem 7.26

Read-back

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

Let $a \le b$ be reals and let $f : \mathbb{R} \to \mathbb{C}$ be continuous on the closed interval $[a,b]$ (relative continuity at each of its points; no assumption elsewhere). Then there exists a sequence $P_0, P_1, \dots$ of polynomials with complex coefficients such that the functions

x \longmapsto P_n(x), \qquad x \in \mathbb{R} \text{ viewed in } \mathbb{C},

converge to $f$ uniformly on $[a,b]$ as $n \to \infty$ .

No bound on the degrees is asserted, and nothing is claimed about approximation outside $[a,b]$ . The degenerate case $a = b$ is allowed.

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