Geometric ergodicity + detailed balance $\Rightarrow$ exponential $\rho$ -mixing (Jones Thm 2(iii))

Open

MarkovChainCLT.rho_mixing_exp_of_geometric_reversible

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$ . Suppose the chain is geometrically ergodic and reversible with respect to $\pi$ (detailed balance, the source's eq. (8)). Then the stationary chain is asymptotically uncorrelated with exponentially fast $\rho$ -mixing: there exist $c \ge 0$ and $\theta > 0$ such that

\rho(n) \;\le\; c\, e^{-\theta n} \qquad (n \ge 1).

Reversibility holds by construction for Metropolis–Hastings samplers, so this result (Roberts–Rosenthal 1997) is the gateway to second-moment CLTs for the most common MCMC algorithms.

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 3** (Roberts–Rosenthal 1997): a geometrically ergodic chain
satisfying detailed balance is asymptotically uncorrelated, with exponentially fast
ρ-mixing. -/

Formal statement

theorem MarkovChainCLT.rho_mixing_exp_of_geometric_reversible {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (hgeo : GeometricallyErgodic P π)
    (hrev : Kernel.IsReversible P π) :
    ∃ c θ : ℝ, 0 ≤ c ∧ 0 < θ ∧ ∀ n : ℕ, 1 ≤ n →
      rhoMixingCoef (chainMeasure P π) (fun i ω => ω i) n ≤ c * Real.exp (-θ * n) := 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 3 (arXiv v2 p. 8; detailed balance = eq. (8)); original: G. O. Roberts & J. S. Rosenthal, Geometric ergodicity and hybrid Markov chains, Electron. Comm. Probab. 2 (1997), Theorem 2.1, plus R. C. Bradley (1986), Theorem 4.2

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), $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$ , with $P^n$ the $n$ -fold iterate ( $P^0$ = identity) and $\operatorname{tv}(\mu,\nu)=\sup\{|\mu(A)-\nu(A)|:A\text{ measurable}\}$ (real supremum, no factor $\tfrac12$ ); (ii) geometric ergodicity, unfolded as: there exist a function $M:X\to\mathbb{R}$ and a real $t$ with $M(x)\ge0$ for all $x$ , $0\le t<1$ , and $\operatorname{tv}(P^n(x,\cdot),\pi)\le M(x)\,t^{\,n}$ for every $x$ and every $n\ge1$ — note that $M$ is required to be neither measurable nor $\pi$ -integrable, only pointwise nonnegative; (iii) Kernel.IsReversible P π, Mathlib's reversibility (detailed-balance) condition: the joint law of one step from stationarity — $x$ drawn from $\pi$ , then $y$ from $P(x,\cdot)$ — is invariant under swapping the two coordinates; equivalently $\int_A P(x,B)\,d\pi(x)=\int_B P(x,A)\,d\pi(x)$ for all measurable $A,B$ . Conclusion: there exist reals $c$ and $\theta$ with $c\ge 0$ (zero allowed) and $\theta>0$ such that for every integer $n\ge1$ (nothing claimed at $n=0$ ), $\rho(n)\ \le\ c\,e^{-\theta n}$ , where $\rho(n)$ is the bundle's ρ-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$ with $\omega_0\sim\pi$ , $\omega_{n+1}\sim P(\omega_n,\cdot)$ ). Unfolded, $\rho(n)$ is the real supremum (sSup) of the set of values $\dfrac{|\operatorname{Cov}(U,V)|}{\sqrt{\operatorname{Var}(U)}\,\sqrt{\operatorname{Var}(V)}}$ over all $k\in\mathbb{N}$ and all real-valued functions $U,V$ on path space such that $U$ is measurable with respect to the σ-algebra generated by coordinates $\{0,\dots,k\}$ , $V$ is measurable with respect to the σ-algebra generated by coordinates $\{k+n,k+n+1,\dots\}$ , and both lie in $L^2(\mathbb P)$ ; the covariance and variances are taken under $\mathbb P$ . Note Lean's division convention: when $\operatorname{Var}(U)=0$ or $\operatorname{Var}(V)=0$ the quotient is the junk value $0$ , so degenerate (e.g. constant) pairs contribute $0$ to the supremum, and the set is therefore nonempty; a real sSup of an unbounded set would be $0$ by convention. The single pair $(c,\theta)$ must serve all $n\ge1$ simultaneously (existential before universal).

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

Geometric ergodicity + detailed balance ⇒\Rightarrow⇒ exponential ρ\rhoρ-mixing (Jones Thm 2(iii))

Geometric ergodicity + detailed balance $\Rightarrow$ exponential $\rho$ -mixing (Jones Thm 2(iii))