Theorem 11.42 — the Riesz–Fischer theorem

Proved

Rudin.ch11_riesz_fischer

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

analysismeasure-theory

$\mathscr{L}^2(\mu)$ is complete: if $\{f_n\}$ is a Cauchy sequence in $\mathscr{L}^2(\mu)$ , then there is an $f \in \mathscr{L}^2(\mu)$ with $\|f_n - f\|_2 \to 0$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 11.42 (Riesz–Fischer): every Cauchy sequence in `ℒ²(μ)` converges in the mean
to a function of `ℒ²(μ)`; that is, `ℒ²(μ)` is complete. -/
theorem ch11_riesz_fischer {X : Type*} [MeasurableSpace X] (μ : Measure X) (f : ℕ → X → ℝ)
    (hmem : ∀ n, MemL2 μ (f n)) (hcauchy : CauchyL2 μ f) :
    ∃ g : X → ℝ, MemL2 μ g ∧ TendstoL2 μ f g := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 11, p. 329, Theorem 11.42

Read-back

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

Let $X$ be a measurable space with measure $\mu$ and let $f_0,f_1,\dots : X \to \mathbb{R}$ be functions such that:

every $f_n$ lies in $\mathcal{L}^2(\mu)$ , i.e. is measurable with integrable square;
the sequence is Cauchy in the $\mathcal{L}^2$ norm: for every $\varepsilon>0$ there is $N$ with

\lVert f_n - f_m\rVert_2 = \sqrt{\int_X (f_n - f_m)^2 d\mu} < \varepsilon \quad\text{for all } m,n \ge N .

Then there exists a function $g : X \to \mathbb{R}$ such that $g \in \mathcal{L}^2(\mu)$ and $f_n \to g$ in the mean:

\lVert f_n - g\rVert_2 \longrightarrow 0 \qquad (n \to \infty).

The limit is produced as an honest function, not an equivalence class, and is not claimed to be unique (any modification on a null set would serve equally); no pointwise or almost-everywhere convergence is asserted.

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