Prove2Me

Reversible indicator decay yields a centered L2L^2 Markov-operator model

Open
MarkovChainCLT.reversible_indicator_decay_centered_L2_operator_model

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

l2markov-operatormaximal-correlationreversibilityspectral-gap

Let PP be stationary and reversible with respect to π\pi, and assume all centered event indicators have the even-lag bound Ct2nC t^{2n}. Then there is a bounded symmetric operator TT on L2(π)L^2(\pi) representing the square of the centered Markov operator, together with a dense linear core DD, such that

0≤ρ(1),ρ(1)2≤∥T∥,0\le\rho(1),\qquad \rho(1)^2\le\|T\|,

and every z∈Dz\in D has power moments bounded by

∣⟨Tnz,z⟩∣≤Cz(t2)n.|\langle T^n z,z\rangle|\le C_z(t^2)^n.

The dense core is generated by centered event indicators. Reversibility gives symmetry, stationarity gives the L2L^2 contraction and identifies correlations with operator moments, and the Markov reduction relates the operator norm to one-step maximal correlation. This is the Markov-specific operator construction separated from the abstract spectral-radius argument.

Preamble
import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure
import Definitions.Def_MixingCoefficients
import Mathlib.MeasureTheory.Function.L2Space
import Mathlib.Analysis.InnerProductSpace.Rayleigh

open MeasureTheory ProbabilityTheory Filter Set
open scoped ENNReal NNReal Topology ProbabilityTheory
Formal statement
theorem MarkovChainCLT.reversible_indicator_decay_centered_L2_operator_model
    {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)) :
    ∃ T : Lp ℝ 2 pi →L[ℝ] Lp ℝ 2 pi,
      (T : Lp ℝ 2 pi →ₗ[ℝ] Lp ℝ 2 pi).IsSymmetric ∧
      0 ≤ rhoMixingCoef (chainMeasure P pi) (fun i omega => omega i) 1 ∧
      (rhoMixingCoef (chainMeasure P pi) (fun i omega => omega i) 1) ^ 2 ≤ ‖T‖ ∧
      ∃ D : Submodule ℝ (Lp ℝ 2 pi), Dense (D : Set (Lp ℝ 2 pi)) ∧
        ∀ z : D, ∃ Cz : ℝ, 0 ≤ Cz ∧
          ∀ n : ℕ, |inner ℝ ((T ^ n) (z : Lp ℝ 2 pi)) (z : Lp ℝ 2 pi)| ≤
            Cz * (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 proof, pp. 6-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