Geometric ergodicity and reversibility give a strict one-step rho contraction

Open

MarkovChainCLT.rhoMixingCoef_one_lt_one_of_geometric_reversible

by Zehao Jin · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainmixingprobabilityreversibilityspectral-gap

Let $(X_n)_{n\ge0}$ be a stationary Harris-ergodic Markov chain with invariant probability law $\pi$ . If its kernel is reversible with respect to $\pi$ and the chain is geometrically ergodic in total variation, then its one-step maximal-correlation coefficient is strictly contractive:

\rho(1)<1.

This is the spectral core of the reversible geometric-ergodicity theorem. Reversibility makes the Markov operator self-adjoint on centered $L^2(\pi)$ ; geometric ergodicity excludes spectrum at modulus one and yields an $L^2$ spectral gap. The coefficient $\rho(1)$ is the corresponding centered operator norm. Combined with the Markov product inequality, this single-lag contraction yields exponential rho-mixing.

Formalization Note HarrisErgodic supplies invariance and pointwise total-variation convergence, while GeometricallyErgodic supplies a common geometric rate with state-dependent prefactor.

Preamble

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

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.rhoMixingCoef_one_lt_one_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 π) :
    rhoMixingCoef (chainMeasure P π) (fun i ω => ω i) 1 < 1 := by sorry

Source

Richard C. Bradley, On Mixing Properties of Reversible Markov Chains, arXiv:1403.4895v1, p. 5, lines discussing the equivalence of rho-mixing, geometric ergodicity, a spectral gap, and rho(1) < 1, https://arxiv.org/abs/1403.4895. See also G. O. Roberts and J. S. Rosenthal, Geometric Ergodicity and Hybrid Markov Chains, Electronic Communications in Probability 2 (1997), Proposition 1 and Theorem 2, pp. 13--15, https://www.probability.ca/jeff/ftpdir/hybrid.pdf.

View graph