An integrable TV rate bounds centered-indicator covariance

Proved

MarkovChainCLT.indicator_even_covariance_decay_of_integrable_rate

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

covariancemarkov-chainspectral-gaptotal-variation

Let $P$ be a Markov kernel with probability law $\pi$ . Suppose that for a nonnegative integrable function $M$ and $t\ge 0$ ,

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

Then for every measurable event $A$ and every $n\ge1$ , the stationary centered-indicator correlation at the even lag $2n$ satisfies

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

This is the direct total-variation input to the reversible spectral-gap argument: an eventwise TV bound becomes exponential decay of the even moments of centered indicators.

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.indicator_even_covariance_decay_of_integrable_rate
    {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P]
    (pi : Measure X) [IsProbabilityMeasure pi]
    (M : X → ℝ) (t : ℝ)
    (hM_nonneg : ∀ x, 0 ≤ M x) (hM_int : Integrable M pi)
    (ht_nonneg : 0 ≤ t)
    (hrate : ErgodicWithRate P pi M (fun n => t ^ n)) :
    ∀ (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| ≤
        (∫ x, M x ∂pi) * t ^ (2 * n) := 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 Relation to Proposition 1, pp. 7-9, https://www.probability.ca/jeff/ftpdir/hybrid.pdf; specialized to centered event indicators and the stated integrable total-variation bound.

View graph