Theorems 8.11-8.12 — best mean-square approximation and Bessel's inequality

Disproved

Rudin.ch08_bessel

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

analysisfourier-analysis

Let $\{\varphi_n\}$ be orthonormal on $[a,b]$ and let $c_m$ be the Fourier coefficients of $f$ . Among all combinations $\sum_{m<n} \gamma_m \varphi_m$ , the choice $\gamma_m = c_m$ minimizes $\int_a^b |f - \sum \gamma_m\varphi_m|^2$ ; and $\sum_{m<n} |c_m|^2 \le \int_a^b |f|^2$ for every $n$ (Bessel's inequality).

Preamble

import Mathlib
import Definitions.Def_Rudin_ch08_fourier

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorems 8.11 and 8.12: among all linear combinations of `φ 0, …, φ (n-1)` the
partial sum of the Fourier series of `f` is the best approximation in the mean square sense, and
Bessel's inequality `∑ |cₘ|² ≤ ∫ |f|²` holds. -/
theorem ch08_bessel (a b : ℝ) (hab : a ≤ b) (φ : ℕ → ℝ → ℂ) (hφ : IsOrthonormalSystem φ a b)
    (f : ℝ → ℂ) (n : ℕ) (γ : ℕ → ℂ) :
    (∫ x in a..b, ‖f x - ∑ m ∈ Finset.range n, genFourierCoeff f φ a b m * φ m x‖ ^ 2) ≤
      (∫ x in a..b, ‖f x - ∑ m ∈ Finset.range n, γ m * φ m x‖ ^ 2) ∧
    (∑ m ∈ Finset.range n, ‖genFourierCoeff f φ a b m‖ ^ 2) ≤ ∫ x in a..b, ‖f x‖ ^ 2 := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8, pp. 187-188, Theorems 8.11 and 8.12

Read-back

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

Let $a \le b$ be reals, let $\varphi_0,\varphi_1,\dots : \mathbb{R}\to\mathbb{C}$ be an orthonormal system on $[a,b]$ — i.e. $\int_a^b \varphi_n \overline{\varphi_m} = 0$ for $m \ne n$ and $\int_a^b \lVert\varphi_n\rVert^2 = 1$ — let $f : \mathbb{R}\to\mathbb{C}$ be any function, let $n \in \mathbb{N}$ and let $\gamma : \mathbb{N}\to\mathbb{C}$ be arbitrary complex numbers. Write $c_m = \int_a^b f \overline{\varphi_m}$ for the Fourier coefficients of $f$ relative to $\varphi$ . Then both:

Least squares optimality.

\int_a^b \Bigl\lVert f(x) - \sum_{m=0}^{n-1} c_m \varphi_m(x) \Bigr\rVert^2 dx \;\le\; \int_a^b \Bigl\lVert f(x) - \sum_{m=0}^{n-1} \gamma_m \varphi_m(x) \Bigr\rVert^2 dx ;

Bessel's inequality.

\sum_{m=0}^{n-1} \lVert c_m \rVert^2 \;\le\; \int_a^b \lVert f(x)\rVert^2 dx .

Both sums run over $m = 0,\dots,n-1$ and both statements are asserted for every $n$ , including $n = 0$ where the sums are empty. No integrability hypothesis is placed on $f$ ; all integrals are oriented interval integrals against Lebesgue measure, which evaluate to $0$ for non-integrable integrands.

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