A countably generated measurable space has a countable generating ring of sets

Proved

MarkovChainCLT.exists_countable_isSetRing_generateFrom

by LukeBernese · Aug 15, 2026 · Mathlib c5ea003 (Lean v4.30.0)

countably-generatedmeasurable-spacemeasure-theoryset-ring

If the $\sigma$ -algebra of $\mathsf X$ is countably generated, then there is a countable family $\mathcal C$ of measurable sets which is a ring of sets (contains $\emptyset$ , closed under union and set difference), contains the whole space, and generates the $\sigma$ -algebra.

Why the ring structure matters. A countable generating family is immediate from the definition of countably generated; a countable generating ring is not, and it is the ring structure that the approximation theorem for measurable sets requires. That theorem — every measurable set is close, in a finite measure, to a member of the ring — is what allows a supremum over all measurable sets to be replaced by a supremum over a countable family. In particular it converts the total variation distance

\|\mu-\nu\| \;=\; \sup_{A \text{ measurable}}|\mu(A)-\nu(A)|

from an uncountable supremum into a countable one, which is what makes $x \mapsto \|P^n(x,\cdot)-\pi\|$ measurable and hence integrable against $\pi$ . Without this, a mixing coefficient cannot be bounded by an integrated convergence rate, and "a Harris ergodic chain is strongly mixing" — where the convergence holds from every starting point but at no uniform rate — has no route.

The construction. Mathlib's countablePartition provides, for a countably generated space, a sequence of finite partitions, each refining the previous one, whose union generates the $\sigma$ -algebra. Take

\mathcal C \;=\; \bigcup_{n} \sigma\bigl(\text{countablePartition}_n\bigr),

the union of the $\sigma$ -algebras generated by the individual partitions. Three observations make this work:

Each level is finite: a set is measurable for the $\sigma$ -algebra of a finite partition exactly when it is a union of parts, so the level injects into the (finite) set of subfamilies of that partition. Hence $\mathcal C$ is a countable union of finite sets.
The levels increase, since each partition refines the previous one. So two members of $\mathcal C$ lie in a common level, where they may be combined: this is what makes $\mathcal C$ closed under union and difference — a union of $\sigma$ -algebras is a ring precisely when the family is directed.
$\mathcal C$ generates: it sits between $\bigcup_n \text{countablePartition}_n$ , which already generates, and the measurable sets.

Note $\mathcal C$ is a ring but not a $\sigma$ -algebra — it is not closed under countable unions, since those can escape every finite level. That is exactly the expected trade-off: countability is bought at the price of only finitary closure, and the approximation theorem is what compensates.

Preamble

import Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
import Mathlib.MeasureTheory.SetSemiring

open MeasureTheory MeasurableSpace Set

Formal statement

theorem MarkovChainCLT.exists_countable_isSetRing_generateFrom {X : Type*}
    [mX : MeasurableSpace X] [MeasurableSpace.CountablyGenerated X] :
    ∃ C : Set (Set X), C.Countable ∧ IsSetRing C ∧ (∀ s ∈ C, MeasurableSet s) ∧
      Set.univ ∈ C ∧ generateFrom C = mX := by sorry

Source

P. Halmos, Measure Theory, Van Nostrand 1950, Sections 5-6 and 13; S. P. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge 2009, Ch. 3 (countably generated state spaces); R. C. Bradley, "Basic Properties of Strong Mixing Conditions", Probability Surveys 2 (2005) 107-144.

View graph