Theorem 11.30 — term-by-term integration of a series of nonnegative functions

Proved

Rudin.ch11_series_integral

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

analysismeasure-theory

If $f_n \ge 0$ are measurable and $f = \sum_n f_n$ , then $\int f\,d\mu = \sum_n \int f_n\,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.30: a series of nonnegative measurable functions may be integrated term by
term. -/
theorem ch11_series_integral {X : Type*} [MeasurableSpace X] (μ : Measure X) (f : ℕ → X → ℝ≥0∞)
    (hf : ∀ n, Measurable (f n)) :
    (∫⁻ x, ∑' n, f n x ∂μ) = ∑' n, ∫⁻ x, f n x ∂μ := by sorry

end Rudin

Source

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

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

\int_X \Bigl(\sum_{n=0}^{\infty} f_n(x)\Bigr) d\mu(x) \;=\; \sum_{n=0}^{\infty} \int_X f_n \, d\mu ,

an equality in $[0,\infty]$ , where the integrals are lower Lebesgue integrals of $[0,\infty]$ -valued functions and both sums are unconditional sums in $[0,\infty]$ (which always exist there).

No finiteness or integrability hypothesis is imposed; both sides may equal $+\infty$ .

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