Prove2Me

A finitely additive measure on a ring of sets extends to all subsets

Proved
FinitelyAdditive.exists_extension_of_isSetRing

by dbenbenn · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

finitely-additive-measuresmeasure-theory

Let XX be a set and R\mathcal{R} a ring of subsets of XX: it contains ∅\emptyset and is closed under finite unions and differences. Let μ:R→[0,∞]\mu : \mathcal{R} \to [0,\infty] satisfy μ(∅)=0\mu(\emptyset) = 0 and μ(s∪t)=μ(s)+μ(t)\mu(s \cup t) = \mu(s) + \mu(t) for disjoint s,t∈Rs, t \in \mathcal{R}. Then there is ν:P(X)→[0,∞]\nu : \mathcal{P}(X) \to [0,\infty], defined on every subset of XX, with

ν(∅)=0,ν(s∪t)=ν(s)+ν(t)  for disjoint s,t⊆X,ν∣R=μ.\nu(\emptyset) = 0, \qquad \nu(s \cup t) = \nu(s) + \nu(t) \ \text{ for disjoint } s, t \subseteq X, \qquad \nu|_{\mathcal{R}} = \mu.

This is the finitely additive extension theorem that Garrido recalls as Carathéodory's Extension Theorem in the statement of the Invariant Extension Theorem: restricting ν\nu to a Boolean algebra of subsets of XX that contains R\mathcal{R} extends μ\mu to that algebra. Only finite additivity is asserted, and ν\nu is not unique. Unlike Carathéodory's σ\sigma-additive extension theorem, it involves no outer measure and no measurability.

Formalization Note. μ\mu is a function on all subsets of XX, but only its values on R\mathcal{R} enter the hypotheses. The ring is Mathlib's IsSetRing, which does not require X∈RX \in \mathcal{R}.

Preamble
import Mathlib
open MeasureTheory
open scoped ENNReal
Formal statement
namespace FinitelyAdditive

theorem exists_extension_of_isSetRing {X : Type*} {R : Set (Set X)} (hR : IsSetRing R)
    (μ : Set X → ℝ≥0∞) (h0 : μ ∅ = 0)
    (hadd : ∀ s ∈ R, ∀ t ∈ R, Disjoint s t → μ (s ∪ t) = μ s + μ t) :
    ∃ ν : Set X → ℝ≥0∞, ν ∅ = 0 ∧ (∀ s t : Set X, Disjoint s t → ν (s ∪ t) = ν s + ν t) ∧
      ∀ s ∈ R, ν s = μ s := by
  sorry

end FinitelyAdditive
Source
A. Garrido, "An introduction to amenable groups", lecture notes, Oxford Advanced Class in Algebra, Michaelmas 2013 (PDF, Feb 2015), p. 7, in the statement of Theorem 2.6: "Recall Carathéodory's Extension Theorem: If R\mathcal{R} is a subring of the boolean algebra A\mathcal{A} and μ\mu is a measure on R\mathcal{R}, then μ\mu can be extended to a measure μˉ\bar\mu on A\mathcal{A}." The measures in the source are finitely additive throughout, and here the Boolean algebra is an algebra of subsets; https://web.archive.org/web/20260805000803/https://www.math.uni-duesseldorf.de/~garrido/amenable.pdf

View graph