An integrable geometric TV rate and reversibility imply strict one-step rho contraction

Open

MarkovChainCLT.rhoMixingCoef_one_lt_one_of_integrable_rate_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 law $\pi$ . Assume there are a nonnegative function $M\in L^1(\pi)$ and a number $t\in[0,1)$ such that, for every state $x$ , every $n\ge1$ ,

d_{\mathrm{TV}}(P^n(x,\cdot),\pi)\le M(x)t^n.

If $P$ is reversible with respect to $\pi$ , then the one-step maximal-correlation coefficient is strictly less than one:

\rho(1)<1.

The integrable pointwise bound first yields exponential absolute regularity under the stationary law. Reversibility identifies the centered Markov operator with a self-adjoint contraction on $L^2(\pi)$ ; the geometric convergence excludes spectrum at modulus one and gives the strict operator-norm contraction represented by $\rho(1)$ .

This theorem is the spectral bridge between the integrable-rate form of geometric ergodicity and exponential rho-mixing.

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_integrable_rate_reversible
    {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P]
    (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π)
    (M : X → ℝ) (t : ℝ)
    (hM_nonneg : ∀ x, 0 ≤ M x) (hM_int : Integrable M π)
    (ht_nonneg : 0 ≤ t) (ht_lt : t < 1)
    (hrate : ErgodicWithRate P π M (fun n => t ^ n))
    (hrev : Kernel.IsReversible P π) :
    rhoMixingCoef (chainMeasure P π) (fun i ω => ω i) 1 < 1 := by sorry

Source

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. See also Richard C. Bradley, On Mixing Properties of Reversible Markov Chains, arXiv:1403.4895v1, p. 5, equivalence of geometric ergodicity, a spectral gap, and rho(1) < 1, https://arxiv.org/abs/1403.4895.

View graph