Theorem 11.24 — the integral is a countably additive set function

Proved

Rudin.ch11_integral_countably_additive

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

analysismeasure-theory

If $f$ is integrable and $E_1, E_2, \dots$ are pairwise disjoint measurable sets with union $E$ , then $\int_E f\,d\mu = \sum_n \int_{E_n} f\,d\mu$ , the series being convergent.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch11_L2

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 11.24: the integral of an integrable function is a countably additive set
function. -/
theorem ch11_integral_countably_additive {X : Type*} [MeasurableSpace X] (μ : Measure X)
    (f : X → ℝ) (hf : Integrable f μ) (E : ℕ → Set X) (hE : ∀ n, MeasurableSet (E n))
    (hdisj : Pairwise (Function.onFun Disjoint E)) :
    HasSum (fun n => ∫ x in E n, f x ∂μ) (∫ x in ⋃ n, E n, f x ∂μ) := by sorry

end Rudin

Source

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

Read-back

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

Let $X$ be a measurable space with measure $\mu$ , let $f : X \to \mathbb{R}$ be integrable with respect to $\mu$ , and let $E_0,E_1,\dots$ be measurable subsets of $X$ that are pairwise disjoint. Then the family of numbers

n \;\longmapsto\; \int_{E_n} f \, d\mu

is summable with sum $\displaystyle\int_{\bigcup_n E_n} f\,d\mu$ — that is, the net of finite partial sums converges unconditionally to that value (a stronger assertion than convergence of the ordered partial sums).

Each integral is the Bochner integral of $f$ restricted to the indicated set. Integrability is assumed on the whole space, which in particular gives integrability on each $E_n$ .

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