Reversible centered-indicator decay bounds one-step maximal correlation

Open

MarkovChainCLT.rhoMixingCoef_one_le_of_reversible_indicator_even_decay

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

markov-chainmaximal-correlationreversibilityspectral-gap

Let $P$ be a stationary Markov kernel reversible with respect to the probability law $\pi$ , and let $0\le t<1$ . Assume there is a finite constant $C\ge0$ such that every centered event indicator has exponentially decaying even-lag correlation:

\left|\int (1_A(x)-\pi(A))\bigl(P^{2n}(x,A)-\pi(A)\bigr)\,\pi(dx)\right| \le Ct^{2n}

for every measurable $A$ and every $n\ge1$ . Then the stationary chain's one-step maximal-correlation coefficient obeys

\rho(1)\le t.

The centered indicators span a dense subspace of centered $L^2(\pi)$ . Reversibility makes the Markov operator self-adjoint, so the displayed even moments control its centered $L^2$ spectrum. The Markov reduction then identifies that operator norm with the one-step maximal correlation.

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_le_of_reversible_indicator_even_decay
    {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P]
    (pi : Measure X) [IsProbabilityMeasure pi]
    (hinv : Kernel.Invariant P pi)
    (t : ℝ) (ht_nonneg : 0 ≤ t) (ht_lt : t < 1)
    (hrev : Kernel.IsReversible P pi)
    (hdecay : ∃ C : ℝ, 0 ≤ C ∧
      ∀ (A : Set X), MeasurableSet A → ∀ n : ℕ, 1 ≤ n →
        |∫ x,
            ((A.indicator (fun _ => (1 : ℝ))) x - pi.real A) *
              (((iterKernel P (2 * n)) x A).toReal - pi.real A) ∂pi| ≤
          C * t ^ (2 * n)) :
    rhoMixingCoef (chainMeasure P pi) (fun i omega => omega i) 1 ≤ t := by sorry

Source

G. O. Roberts and J. S. Rosenthal, Geometric Ergodicity and Hybrid Markov Chains, Electronic Communications in Probability 2 (1997), Theorem 2 and proof, pp. 7-9, https://www.probability.ca/jeff/ftpdir/hybrid.pdf; Richard C. Bradley, On Mixing Properties of Reversible Markov Chains, arXiv:1403.4895v1, p. 4, eq. (1.10), https://arxiv.org/abs/1403.4895.

View graph