Theorem 11.32 — Lebesgue's dominated convergence theorem

Proved

Rudin.ch11_dominated_convergence

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

analysismeasure-theory

If measurable functions $f_n$ converge pointwise to $f$ and satisfy $|f_n| \le g$ for an integrable $g$ , then $f$ is integrable and $\int f_n\,d\mu \to \int f\,d\mu$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 11.32 (Lebesgue's dominated convergence theorem): if measurable functions
`f n` converge pointwise to `g` and are dominated by an integrable `h`, then `g` is
integrable and the integrals converge. -/
theorem ch11_dominated_convergence {X : Type*} [MeasurableSpace X] (μ : Measure X)
    (f : ℕ → X → ℝ) (g h : X → ℝ) (hf : ∀ n, Measurable (f n))
    (hdom : ∀ n, ∀ x, |f n x| ≤ h x) (hh : Integrable h μ)
    (hconv : ∀ x, Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
    Integrable g μ ∧ Tendsto (fun n => ∫ x, f n x ∂μ) atTop (𝓝 (∫ x, g x ∂μ)) := by sorry

end Rudin

Source

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

Read-back

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

Let $X$ be a measurable space with measure $\mu$ , let $f_0,f_1,\dots : X \to \mathbb{R}$ be measurable, and let $g, h : X\to\mathbb{R}$ . Assume:

$|f_n(x)| \le h(x)$ for every index $n$ and every point $x$ (pointwise everywhere domination);
$h$ is integrable with respect to $\mu$ ;
for every $x$ , $f_n(x) \to g(x)$ as $n \to \infty$ (pointwise convergence everywhere).

Then both:

$g$ is integrable with respect to $\mu$ ;
$\displaystyle \int_X f_n \, d\mu \longrightarrow \int_X g \, d\mu$ as $n\to\infty$ .

Measurability of $g$ is not assumed (it follows from the pointwise limit). No almost-everywhere weakening is used: both the domination and the convergence are required at every point.

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