Theorem 11.45 — Parseval's identity for a complete orthonormal system

Proved

Rudin.ch11_parseval_complete

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

analysisfourier-analysismeasure-theory

Let $\{\varphi_n\}$ be a complete orthonormal system in $\mathscr{L}^2(\mu)$ and let $c_n = \int f\varphi_n\,d\mu$ be the Fourier coefficients of $f \in \mathscr{L}^2(\mu)$ . Then $\sum_n c_n^2 = \int f^2\,d\mu$ ; the Fourier series of $f$ converges to $f$ in the mean.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 11.45: if `{φₙ}` is a complete orthonormal set in `ℒ²(μ)` and `cₙ` are the
Fourier coefficients of `f ∈ ℒ²(μ)`, then `∑ cₙ² = ∫ f² dμ` (Parseval's identity). -/
theorem ch11_parseval_complete {X : Type*} [MeasurableSpace X] (μ : Measure X) (φ : ℕ → X → ℝ)
    (hmem : ∀ n, MemL2 μ (φ n))
    (horth : ∀ m n, m ≠ n → (∫ x, φ m x * φ n x ∂μ) = 0)
    (hnorm : ∀ n, (∫ x, (φ n x) ^ 2 ∂μ) = 1)
    (hcomplete : ∀ g : X → ℝ, MemL2 μ g → (∀ n, (∫ x, g x * φ n x ∂μ) = 0) → L2Norm μ g = 0)
    (f : X → ℝ) (hf : MemL2 μ f) (c : ℕ → ℝ) (hc : ∀ n, c n = ∫ x, f x * φ n x ∂μ) :
    Tendsto (fun N => ∑ n ∈ Finset.range N, (c n) ^ 2) atTop (𝓝 (∫ x, (f x) ^ 2 ∂μ)) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 11, p. 331, Theorems 11.43 and 11.45

Read-back

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

Let $X$ be a measurable space with measure $\mu$ and let $\varphi_0,\varphi_1,\dots : X \to \mathbb{R}$ satisfy:

each $\varphi_n$ lies in $\mathcal{L}^2(\mu)$ (measurable with integrable square);
orthogonality: $\int_X \varphi_m \varphi_n \, d\mu = 0$ whenever $m \ne n$ ;
normalization: $\int_X \varphi_n^2 \, d\mu = 1$ for every $n$ ;
completeness: for every $g \in \mathcal{L}^2(\mu)$ , if $\int_X g\,\varphi_n \, d\mu = 0$ for all $n$ , then $\lVert g \rVert_2 = 0$ (the norm vanishes; $g$ itself need not be the zero function).

Let $f \in \mathcal{L}^2(\mu)$ and let $c : \mathbb{N}\to\mathbb{R}$ be defined by the hypothesis $c_n = \int_X f\,\varphi_n\,d\mu$ for every $n$ . Then

\sum_{n=0}^{N-1} c_n^{2} \;\longrightarrow\; \int_X f^2 \, d\mu \qquad (N \to \infty),

i.e. the partial sums of the squares of the Fourier coefficients converge to the integral of $f^2$ .

The partial sum over $n < N$ omits the term $c_N$ ; the limit is asserted for the ordered partial sums.

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