Theorem 8.15 — uniform approximation by trigonometric polynomials

Proved

Rudin.ch08_trig_approximation

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

analysisapproximationfourier-analysis

If $f$ is continuous with period $2\pi$ and $\varepsilon > 0$ , there is a trigonometric polynomial $P$ with $|P(x) - f(x)| < \varepsilon$ for all real $x$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch08_fourier

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.15: a continuous `2π`-periodic function can be uniformly approximated by
trigonometric polynomials. -/
theorem ch08_trig_approximation (f : ℝ → ℂ) (hcont : Continuous f) (hper : HasPeriodTwoPi f)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ P : ℝ → ℂ, IsTrigPolynomial P ∧ ∀ x : ℝ, ‖P x - f x‖ < ε := by sorry

end Rudin

Source

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

Read-back

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

Let $f : \mathbb{R}\to\mathbb{C}$ be continuous on all of $\mathbb{R}$ and satisfy $f(x+2\pi) = f(x)$ for every real $x$ , and let $\varepsilon > 0$ . Then there exists a function $P : \mathbb{R}\to\mathbb{C}$ which is a trigonometric polynomial — that is, for some $N \in \mathbb{N}$ and coefficients $c_{-N},\dots,c_N \in \mathbb{C}$ one has $P(x) = \sum_{n=-N}^{N} c_n e^{inx}$ for all real $x$ — such that

\lVert P(x) - f(x) \rVert < \varepsilon \qquad \text{for every } x \in \mathbb{R}.

The approximation is uniform over the whole real line (equivalently, over one period), with a strict inequality, and $N$ may depend on $\varepsilon$ .

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