Theorem 11.28 — Lebesgue's monotone convergence theorem

Proved

Rudin.ch11_monotone_convergence

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

analysismeasure-theory

If $0 \le f_1 \le f_2 \le \cdots$ are measurable and $f_n(x) \to f(x)$ for every $x$ , then $\int f_n\,d\mu \to \int f\,d\mu$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory
open scoped ENNReal

Formal statement

namespace Rudin

/-- Rudin, Theorem 11.28 (Lebesgue's monotone convergence theorem): if `0 ≤ f 0 ≤ f 1 ≤ ⋯` are
measurable and converge pointwise to `g`, then the integrals converge to the integral of
`g`. -/
theorem ch11_monotone_convergence {X : Type*} [MeasurableSpace X] (μ : Measure X)
    (f : ℕ → X → ℝ≥0∞) (hf : ∀ n, Measurable (f n)) (hmono : ∀ x, Monotone fun n => f n x)
    (g : X → ℝ≥0∞) (hg : ∀ x, Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
    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. 319, Theorem 11.28

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 [0,\infty]$ be measurable functions into the extended nonnegative reals such that for every $x$ the sequence $n \mapsto f_n(x)$ is monotone non-decreasing. Let $g : X \to [0,\infty]$ be such that for every $x$ , $f_n(x) \to g(x)$ in $[0,\infty]$ (convergence in the order topology, which includes tending to $+\infty$ ). Then

\int_X^{-} f_n \, d\mu \;\longrightarrow\; \int_X^{-} g\, d\mu \qquad (n\to\infty),

where $\int^{-}$ denotes the lower Lebesgue integral of a $[0,\infty]$ -valued function, and convergence is again in $[0,\infty]$ .

Nonnegativity is automatic from the codomain; no measurability of $g$ is assumed as a hypothesis, and no finiteness of any integral is required.

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