$\alpha(n) \le \gamma(n)\, E_\pi M$ from a total-variation rate (Jones Thm 2(ii))

Proved

MarkovChainCLT.alpha_mixing_le_tv_rate

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

markov-chainsmcmcmixing-processesprobability

Let $X$ be a Markov chain with transition kernel $P$ , Harris ergodic with invariant probability $\pi$ , and suppose the total-variation rate bound $\|P^n(x, \cdot) - \pi\| \le M(x)\, \gamma(n)$ holds for all $x$ and all $n \ge 1$ , where $M \ge 0$ is integrable with respect to $\pi$ and $\gamma \ge 0$ . Then the strong mixing coefficients of the stationary chain satisfy

\alpha(n) \;\le\; \gamma(n) \int M \, d\pi \qquad (n \ge 1).

This quantitative bound turns any total-variation convergence rate (geometric, polynomial, …) into a mixing rate, and is the step through which the corollaries of the mission consume the classical sequence CLTs. The source records the consequence $\alpha(n) = O(\gamma(n))$ ; the sharp inequality stated here is what its derivation gives.

Formalization Note "Harris ergodic" is encoded by its total-variation characterization: $\pi$ is invariant for $P$ and $\|P^n(x, \cdot) - \pi\| \to 0$ for every starting point $x$ (equivalent to the classical aperiodic, $\psi$ -irreducible, positive Harris recurrent definition; the "every $x$ " quantifier is exactly the Harris property). Convergence in distribution is weak convergence of laws, and $N(0, 0)$ is read as the point mass at $0$ , which absorbs the source's " $\sigma_f^2 > 0$ " caveat.

Preamble

import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

/-- **Theorem 2, part 2**: if the chain has total-variation rate `γ` with constant
`M` and `E_π M < ∞`, then the strong mixing coefficients of the stationary chain
satisfy `α(n) ≤ γ(n) E_π M` for all `n ≥ 1` (Jones 2004, §3; the paper states the
consequence `α(n) = O(γ(n))`). -/

Formal statement

theorem MarkovChainCLT.alpha_mixing_le_tv_rate {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π)
    (M : X → ℝ) (hM0 : ∀ x, 0 ≤ M x) (hM : Integrable M π)
    (γ : ℕ → ℝ) (hγ0 : ∀ n, 0 ≤ γ n) (hrate : ErgodicWithRate P π M γ) :
    ∀ n : ℕ, 1 ≤ n →
      alphaMixingCoef (chainMeasure P π) (fun i ω => ω i) n ≤ γ n * ∫ x, M x ∂π := by sorry

Source

G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Theorem 2, part 2 (arXiv v2 p. 8; Section 3 derivation via the coupling inequality, eq. (7))

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Let $X$ be a type with a σ-algebra (no countable-generation assumption here), $P$ a Markov kernel from $X$ to itself (each $P(x,\cdot)$ a probability measure), and $\pi$ a probability measure on $X$ . Hypotheses: (i) Harris ergodicity: $\pi$ is invariant for $P$ and for every $x\in X$ , $\operatorname{tv}(P^n(x,\cdot),\pi)\to0$ , where $P^n$ is the $n$ -fold iterate ( $P^0$ = identity) and $\operatorname{tv}(\mu,\nu)=\sup\{|\mu(A)-\nu(A)|:A\text{ measurable}\}$ (real supremum, measure values converted to reals, no factor $\tfrac12$ ); (ii) $M:X\to\mathbb{R}$ with $M(x)\ge0$ for every $x$ and $M$ integrable with respect to $\pi$ (Integrable: a.e. strongly measurable and $\int|M|\,d\pi<\infty$ ); (iii) $\gamma:\mathbb{N}\to\mathbb{R}$ with $\gamma(n)\ge0$ for every $n$ ; (iv) the rate condition: for every $x\in X$ and every integer $n\ge1$ , $\operatorname{tv}(P^n(x,\cdot),\pi)\le M(x)\,\gamma(n)$ (nothing is claimed at $n=0$ ). Conclusion: for every integer $n\ge 1$ , $\alpha(n)\ \le\ \gamma(n)\cdot\int M\,d\pi$ (a non-strict inequality; $n=0$ excluded), where $\alpha(n)$ is the α-mixing coefficient of the coordinate process $\omega\mapsto\omega_i$ under the stationary path measure $\mathbb P$ — the Ionescu–Tulcea measure on $\mathbb{N}\to X$ of the chain started from $\pi$ itself ( $\omega_0\sim\pi$ , $\omega_{n+1}\sim P(\omega_n,\cdot)$ ). Unfolded, $\alpha(n)$ is the real supremum (sSup) of the set of numbers $|\mathbb P(A\cap B)-\mathbb P(A)\,\mathbb P(B)|$ over all $k\in\mathbb{N}$ , all $A$ measurable for the σ-algebra generated by coordinates $\{0,\dots,k\}$ , and all $B$ measurable for the σ-algebra generated by coordinates $\{k+n,k+n+1,\dots\}$ (measure values converted to reals; the set contains $0$ , e.g. $A=B=\emptyset$ ; by convention a real sSup of an empty or unbounded set is $0$ ). The bound's right-hand side is the product of the rate value $\gamma(n)$ with the Bochner integral $\int M\,d\pi$ .

Human review

Endorsed by Community (Bot) · Aug 15, 2026
Endorsed by Shuze Chen · Aug 15, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

α(n)≤γ(n) EπM\alpha(n) \le \gamma(n)\, E_\pi Mα(n)≤γ(n)Eπ​M from a total-variation rate (Jones Thm 2(ii))

$\alpha(n) \le \gamma(n)\, E_\pi M$ from a total-variation rate (Jones Thm 2(ii))