The strong mixing coefficient $\alpha(n)$ is realised, up to a factor 2, by one countable family of sets at every lag

Proved

MarkovChainCLT.exists_countable_alpha_witnesses

by Nickrobbins95 · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixingprobability

Let $(\Omega,\mathcal{F},P)$ be a probability space and let $Y_0,Y_1,\dots$ be any sequence of random elements of a measurable space $E$ (no measurability of the $Y_i$ is assumed). The strong mixing coefficient $\alpha(n)$ is by definition a supremum over an uncountable family of pairs of events, each measurable with respect to a $\sigma$ -algebra generated by the full $\sigma$ -algebra of $E$ .

This theorem asserts that the coefficient is already realised, up to a factor $2$ , by a single countable family of measurable subsets of the state space, simultaneously at every lag. Precisely: there exist a countable family $\mathcal{C}$ of measurable subsets of $E$ , split points $K_n$ , and events $A_n$ (past) and $B_n$ (future) with $A_n$ measurable for $\sigma(Y_i : i \le K_n)$ and $B_n$ measurable for $\sigma(Y_i : i \ge K_n + n)$ , both computed over the countably generated $\sigma$ -algebra $\sigma(\mathcal{C})$ rather than over the full $\sigma$ -algebra of $E$ , such that

\alpha(n) \;\le\; 2\,\bigl|P(A_n \cap B_n) - P(A_n)P(B_n)\bigr| \qquad \text{for every } n.

The bound is purely multiplicative: there is no additive slack term. The factor $2$ appears because the supremum defining $\alpha(n)$ need not be attained, so a single pair of events per lag can only be required to capture a fixed proportion of it; any constant $>1$ would serve, and $2$ is the convenient choice, absorbed into the constant of any downstream geometric bound.

The proof rests on the standard fact that every set measurable for a generated $\sigma$ -algebra already uses only countably many generators; each individual event is pulled back to a countable generating family, and $\mathcal{C}$ is the countable union over lags of those families.

The point of the statement is measurability: it reduces any question about $\alpha(n)$ on an arbitrary state space to the countably generated case, which is where the standard machinery of Markov chain mixing theory applies.

Preamble

import Definitions.Def_MixingCoefficients
open MeasureTheory ProbabilityTheory MeasurableSpace
open scoped ENNReal NNReal ProbabilityTheory

Formal statement

namespace MarkovChainCLT

theorem exists_countable_alpha_witnesses {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : ℕ → Ω → E) :
    ∃ (𝒞 : Set (Set E)) (K : ℕ → ℕ) (A B : ℕ → Set Ω),
      𝒞.Countable ∧ (∀ S ∈ 𝒞, MeasurableSet S) ∧
      (∀ n, MeasurableSet[@processSigma Ω E (generateFrom 𝒞) Y (Set.Iic (K n))] (A n)) ∧
      (∀ n, MeasurableSet[@processSigma Ω E (generateFrom 𝒞) Y (Set.Ici (K n + n))] (B n)) ∧
      (∀ n, alphaMixingCoef P Y n ≤
        2 * |(P (A n ∩ B n)).toReal - (P (A n)).toReal * (P (B n)).toReal|) := by sorry

end MarkovChainCLT

Source

Galin L. Jones, On the Markov Chain Central Limit Theorem, Probability Surveys 1 (2004) 299-320, Section 3, Definition 1 (definition of the strong mixing coefficient alpha(n)); the countable-generation step is the standard fact that a generated sigma-algebra is the union of the sigma-algebras generated by its countable subfamilies (P. R. Halmos, Measure Theory, Springer GTM 18, Section 13).

View graph

The strong mixing coefficient α(n)\alpha(n)α(n) is realised, up to a factor 2, by one countable family of sets at every lag

The strong mixing coefficient $\alpha(n)$ is realised, up to a factor 2, by one countable family of sets at every lag