Theorem 11.38 — continuous functions are dense in $\mathscr{L}^2[a,b]$

Proved

Rudin.ch11_continuous_dense

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

analysisapproximationmeasure-theory

If $f \in \mathscr{L}^2$ on $[a, b]$ and $\varepsilon > 0$ , there is a continuous function $g$ with $\|f - g\|_2 < \varepsilon$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 11.38: the continuous functions are dense in `ℒ²` on `[a, b]`: for
`f ∈ ℒ²` on `[a, b]` and `ε > 0` there is a continuous `g` with `‖f - g‖₂ < ε`. -/
theorem ch11_continuous_dense (a b : ℝ) (hab : a ≤ b) (f : ℝ → ℝ)
    (hf : MemL2 (volume.restrict (Set.Icc a b)) f) (ε : ℝ) (hε : 0 < ε) :
    ∃ g : ℝ → ℝ, Continuous g ∧
      L2Norm (volume.restrict (Set.Icc a b)) (fun x => f x - g x) < ε := by sorry

end Rudin

Source

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

Read-back

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

Let $a \le b$ be reals, let $\mu$ be Lebesgue measure restricted to the interval $[a,b]$ , let $f : \mathbb{R}\to\mathbb{R}$ belong to $\mathcal{L}^2(\mu)$ — i.e. $f$ is measurable and $\int_{[a,b]} f^2 < \infty$ — and let $\varepsilon > 0$ . Then there exists a function $g : \mathbb{R}\to\mathbb{R}$ which is continuous on all of $\mathbb{R}$ and satisfies

\lVert f - g \rVert_2 \;=\; \sqrt{\int_{[a,b]} \bigl(f(x)-g(x)\bigr)^2 dx} \;<\; \varepsilon .

The approximation is measured only over $[a,b]$ ; nothing is asserted about the behaviour of $g$ outside, nor about $g$ having compact support or being bounded. The square root returns $0$ on negative arguments and the integral returns $0$ for non-integrable integrands, so the inequality is between a nonnegative real and $\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

Theorem 11.38 — continuous functions are dense in L2[a,b]\mathscr{L}^2[a,b]L2[a,b]

Theorem 11.38 — continuous functions are dense in $\mathscr{L}^2[a,b]$