Total variation is attained on a generating ring of sets

Proved

MarkovChainCLT.tvDist_le_sSup_of_isSetRing

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

measurabilitymeasure-theorymixingtotal-variation

Let $\mu,\nu$ be finite measures on $\mathsf X$ and let $\mathcal C$ be a ring of measurable sets which generates the $\sigma$ -algebra and covers the space modulo $\mu+\nu$ -null sets. Then

\|\mu-\nu\| \;:=\; \sup_{A \text{ measurable}}|\mu(A)-\nu(A)| \;\le\; \sup_{A \in \mathcal C}|\mu(A)-\nu(A)|.

Since the reverse inequality is trivial, the total variation distance is already attained on the generating ring: no measurable set does better than the ring can approximate.

Why this is the key to measurability. The total variation distance is defined as a supremum over all measurable sets — an uncountable index set — so a function like $x \mapsto \|P^n(x,\cdot)-\pi\|$ has no obvious measurability. Yet exactly that measurability is what is needed to write a mixing bound as an integral, $\alpha(n) \le \int \|P^n(x,\cdot)-\pi\|\,\mathrm{d}\pi(x)$ , and hence to conclude $\alpha(n)\to 0$ from a chain that converges from every starting point but at no uniform rate — the content of "a Harris ergodic chain is strongly mixing".

On a countably generated space one can take $\mathcal C$ countable (for instance the union of the finite algebras generated by the canonical decreasing sequence of finite partitions, which is a ring because those algebras increase). This theorem then turns the defining supremum into a countable one, and a countable supremum of measurable functions is measurable. That is precisely why the standard statement of the theorem carries a countably-generated hypothesis on the state space.

Proof. Fix a measurable $A$ and $\varepsilon>0$ . By the approximation theorem for a generating ring, applied to the finite measure $\mu+\nu$ , there is $t \in \mathcal C$ with $(\mu+\nu)(t \,\Delta\, A) < \varepsilon/2$ , hence $\mu(t\,\Delta\,A)$ and $\nu(t\,\Delta\,A)$ are each below $\varepsilon/2$ .

For any finite measure $\rho$ , splitting $A$ and $t$ along $A\cap t$ gives $\rho(A)-\rho(t) = \rho(A\setminus t)-\rho(t\setminus A)$ , whence

|\rho(A)-\rho(t)| \;\le\; \rho(A\setminus t)+\rho(t\setminus A) \;=\; \rho(t\,\Delta\,A).

Therefore

\bigl|\mu(A)-\nu(A)\bigr| - \bigl|\mu(t)-\nu(t)\bigr| \;\le\; |\mu(A)-\mu(t)| + |\nu(A)-\nu(t)| \;\le\; \mu(t\,\Delta\,A)+\nu(t\,\Delta\,A) \;<\; \varepsilon,

so $|\mu(A)-\nu(A)| \le \sup_{\mathcal C} + \varepsilon$ . As $\varepsilon$ was arbitrary the bound holds without it, and taking the supremum over $A$ finishes. The supremum over $\mathcal C$ is a legitimate real number because the defining set is bounded above by $\mu(\mathsf X)+\nu(\mathsf X)$ and contains $0$ (via $\emptyset \in \mathcal C$ ).

Preamble

import Definitions.Def_TotalVariationDist
import Mathlib.MeasureTheory.Measure.MeasuredSets

open MeasureTheory MeasurableSpace
open MarkovChainCLT
open scoped ENNReal NNReal symmDiff

Formal statement

theorem MarkovChainCLT.tvDist_le_sSup_of_isSetRing {X : Type*} [mX : MeasurableSpace X]
    (μ ν : Measure X) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (C : Set (Set X)) (hC : IsSetRing C) (hCm : ∀ s ∈ C, MeasurableSet s)
    (hcov : ∃ D : Set (Set X), D.Countable ∧ D ⊆ C ∧ (μ + ν) (⋃₀ D)ᶜ = 0)
    (hgen : mX = generateFrom C) :
    tvDist μ ν ≤ sSup {r | ∃ A ∈ C, r = |(μ A).toReal - (ν A).toReal|} := by sorry

Source

P. Halmos, Measure Theory, Van Nostrand 1950, Section 13 (approximation by a generating ring); I. A. Ibragimov and Yu. V. Linnik, Independent and Stationary Sequences of Random Variables, Wolters-Noordhoff 1971, Ch. 17; R. C. Bradley, "Basic Properties of Strong Mixing Conditions", Probability Surveys 2 (2005) 107-144; S. P. Meyn and R. L. Tweedie, Markov Chains and Stochastic Stability, 2nd ed., Cambridge 2009, Ch. 16.

View graph