Theorem 11.31 — Fatou's theorem

Proved

Rudin.ch11_fatou

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

analysismeasure-theory

If $f_n \ge 0$ are measurable and $f = \liminf_n f_n$ , then $\int f\,d\mu \le \liminf_n \int f_n\,d\mu$ . Strict inequality may occur.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory
open scoped ENNReal

Formal statement

namespace Rudin

/-- Rudin, Theorem 11.31 (Fatou's theorem): for nonnegative measurable functions, the integral of
the lower limit is at most the lower limit of the integrals. -/
theorem ch11_fatou {X : Type*} [MeasurableSpace X] (μ : Measure X) (f : ℕ → X → ℝ≥0∞)
    (hf : ∀ n, Measurable (f n)) :
    (∫⁻ x, liminf (fun n => f n x) atTop ∂μ) ≤ liminf (fun n => ∫⁻ x, f n x ∂μ) atTop := by sorry

end Rudin

Source

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

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. Then

\int_X \liminf_{n\to\infty} f_n(x)\, d\mu(x) \;\le\; \liminf_{n\to\infty} \int_X f_n \, d\mu ,

an inequality in $[0,\infty]$ , the integrals being lower Lebesgue integrals and both lower limits taken in $[0,\infty]$ (where they always exist).

The inequality goes only in this direction, and no integrability, domination or convergence hypothesis is imposed.

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