Motivation

Chapter 11 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) replaces the Riemann integral of Chapter 6 with the Lebesgue integral, and the reward is a theory of integration whose limit theorems have no superfluous hypotheses and whose space of square-integrable functions is complete. The chapter runs from set functions and outer measures, through the Carathéodory construction of Lebesgue measure, measurable functions and the integral, to the convergence theorems (monotone convergence, Fatou, dominated convergence) and finally to the space $\mathscr{L}^2(\mu)$ and the Riesz–Fischer theorem (Theorem 11.42):

$$\text{every Cauchy sequence in } \mathscr{L}^2(\mu) \text{ converges in the mean to an element of } \mathscr{L}^2(\mu).$$

That completeness is what makes $\mathscr{L}^2$ a Hilbert space, and it is the reason the Fourier series of Chapter 8 converge in the mean to the functions they represent.

This mission is the eleventh and last in a series formalizing Rudin Chapters 1–11. It uses the Riemann–Stieltjes integral of Mission VI (for Theorem 11.33, comparing the two integrals) and the trigonometric Fourier series of Mission VIII (for the $\mathscr{L}^2$ reading of Parseval's theorem).

Setting

A set function on a ring $\mathscr{R}$ of sets is countably additive if it takes the value $\sum \phi(A_n)$ on a countable disjoint union. Rudin constructs an outer measure $\mu^*$ from such a $\phi$ by covering with elementary sets and taking an infimum, calls a set measurable when it is approximable by elementary sets in the metric $d(A, B) = \mu^*(A \triangle B)$, and proves that the measurable sets form a $\sigma$-algebra on which $\mu^*$ is countably additive (Theorem 11.10). A real function $f$ is measurable when $\{x : f(x) > a\}$ is measurable for every $a$, and the integral $\int_E f\,d\mu$ is defined first for simple functions, then for nonnegative measurable functions as a supremum, and then for general $f$ by $f = f^+ - f^-$.

The space $\mathscr{L}^2(\mu)$ consists of the measurable $f$ with $\int |f|^2 d\mu < \infty$, normed by $\|f\|_2 = (\int |f|^2 d\mu)^{1/2}$; a sequence $\{f_n\}$ converges in the mean to $f$ if $\|f_n - f\|_2 \to 0$.

Mathlib's measure theory is used wherever it is mathematically the same object: MeasureTheory.OuterMeasure and its Carathéodory $\sigma$-algebra, MeasurableSet, Measurable, the lower Lebesgue integral ∫⁻ for nonnegative extended-real functions, the Bochner integral ∫ and Integrable for the general case. What is set up freshly is Rudin's $\mathscr{L}^2$ of functions — Rudin.MemL2, Rudin.L2Norm, Rudin.CauchyL2, Rudin.TendstoL2 — rather than Mathlib's quotient space Lp, because the Riesz–Fischer theorem as Rudin states it produces an honest limit function, and the ε-N phrasing of Cauchyness and of mean convergence is part of the statement.

Formalization targets

Goal — the Riesz–Fischer theorem (Theorem 11.42)

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

Rudin's proof extracts a subsequence with $\|f_{n_{k+1}} - f_{n_k}\|_2 < 2^{-k}$, sums the telescoping series, uses the monotone convergence theorem and the Schwarz inequality to show that the sum converges almost everywhere, and identifies the pointwise limit as the mean limit of the whole sequence. Every ingredient is a milestone of this mission.

Milestones

$$\text{the measurable sets of an outer measure form a } \sigma\text{-algebra on which it is countably additive} \qquad (11.10)$$ $$\sup_n f_n \text{ and } \limsup_n f_n \text{ are measurable} \qquad (11.17)$$ $$|f|,\ f+g,\ fg \text{ are measurable} \qquad (11.16,\ 11.18)$$ $$E \mapsto \int_E f\,d\mu \text{ is countably additive} \qquad (11.24)$$ $$\left|\int f\,d\mu\right| \le \int |f|\,d\mu \qquad (11.26,\ 11.27)$$ $$\int \lim_n f_n \,d\mu = \lim_n \int f_n\,d\mu \ \text{ for } 0 \le f_1 \le f_2 \le \cdots \qquad (11.28)$$ $$\int \sum_n f_n \,d\mu = \sum_n \int f_n\,d\mu \ \text{ for } f_n \ge 0 \qquad (11.30)$$ $$\int \liminf_n f_n\,d\mu \le \liminf_n \int f_n\,d\mu \qquad (11.31)$$ $$\text{dominated convergence} \qquad (11.32)$$ $$\text{Riemann-integrable} \Rightarrow \text{Lebesgue-integrable, with the same integral} \qquad (11.33)$$ $$\left|\int fg\,d\mu\right| \le \|f\|_2\,\|g\|_2 \qquad (11.35)$$ $$\text{continuous functions are dense in } \mathscr{L}^2[a,b] \qquad (11.38)$$ $$\sum_n c_n^2 = \int f^2 d\mu \text{ for a complete orthonormal system} \qquad (11.45)$$

Significance

The Lebesgue theory is the point at which analysis acquires limit theorems that do not require uniform convergence. Monotone convergence, Fatou's lemma and dominated convergence are the three statements that make the integral usable in probability, in Fourier analysis and in the theory of partial differential equations, and the Riesz–Fischer theorem is what makes $\mathscr{L}^2$ a Hilbert space and therefore the natural home of Fourier expansions: Parseval's identity (11.45) is the assertion that the Fourier coefficient map is an isometry onto $\ell^2$.

Theorem 11.33 is the bridge back to the earlier chapters — every Riemann-integrable function is Lebesgue-integrable with the same integral, and a bounded function on $[a, b]$ is Riemann-integrable exactly when it is continuous almost everywhere — so the two halves of the book agree wherever both apply.

Mathlib has an extensive measure theory and proves many of these results in considerable generality. This mission's contribution is to state them in Rudin's formulation, for Rudin's $\mathscr{L}^2$ of functions and with his explicit ε-N definitions, so that the chapter is available as a coherent, self-contained unit that matches the textbook line by line and links back to the Riemann–Stieltjes integral of Mission VI.

Difficulty

Individually, most milestones will reduce to Mathlib results after the correct dictionary is in place, and the interesting work is exactly in that translation: Rudin's measurability ({x : f(x) > a} measurable) versus Mathlib's Measurable, Rudin's integral of a nonnegative function versus ∫⁻ with values in ℝ≥0∞, Rudin's $\mathscr{L}^2$ of genuine functions versus Lp as a quotient by almost-everywhere equality. The last of these is what makes the goal theorem nontrivial to derive: Mathlib's completeness of Lp gives a limit class, and one must choose a measurable representative and verify Rudin's mean convergence with the concrete norm Rudin.L2Norm, which is Real.sqrt (∫ f²) and not an ENNReal quantity.

Theorem 11.33 (Riemann implies Lebesgue) and Theorem 11.38 (density of continuous functions) are the two other places where real work is required: the first has to connect the Chapter 6 definition of the Riemann integral with intervalIntegral, and the second is an approximation argument.

Formalization scope

Conventions fixed by this mission:

• Measure-theoretic vocabulary is Mathlib's: MeasureTheory.Measure, MeasurableSet, Measurable, Integrable, ∫⁻ x, f x ∂μ for nonnegative ℝ≥0∞-valued integrands and ∫ x, f x ∂μ for the general real case. Rudin's Carathéodory construction is MeasureTheory.OuterMeasure.caratheodory.
• Statements about suprema and upper limits of sequences of functions (11.17), and about term-by-term integration of series (11.30) and Fatou's theorem (11.31), use ℝ≥0∞-valued functions, matching Rudin's use of extended real values there.
• Rudin.MemL2 μ f is "f is measurable and f² is integrable"; Rudin.L2Norm μ f is Real.sqrt (∫ x, (f x)^2 ∂μ); Rudin.CauchyL2 and Rudin.TendstoL2 are Rudin's ε-N Cauchy condition and mean convergence. No quotient is taken, so the goal theorem produces a function.
• Theorem 11.33 is stated with Rudin.RiemannIntegrable and Rudin.RiemannIntegral from Mission VI, so the two integrals are literally compared.
• Parseval (11.45) is stated for an arbitrary complete orthonormal system in $\mathscr{L}^2(\mu)$, completeness being phrased as "a function orthogonal to every $\varphi_n$ has norm zero"; the trigonometric case is Theorem 8.16 of Mission VIII.

Contributions of the convergence theorems (11.28, 11.31, 11.32) and of the Schwarz inequality (11.35) are especially useful, since the goal theorem consumes them directly.

Selected references

• Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 11 (pp. 300–332).
• Walter Rudin, Real and Complex Analysis, 3rd edition, McGraw-Hill, 1987, Chapters 1–3.