Prove2Me

The centered L2L^2 operator of a stationary reversible Markov chain

Open
MarkovChainCLT.stationary_reversible_centered_L2_operator

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

l2markov-operatormaximal-correlationreversibility

Let PP preserve the probability law π\pi and be reversible with respect to it. Then the stationary chain has a bounded centered Markov operator KK on real L2(π)L^2(\pi). It is self-adjoint, kills constants, and dominates the one-step maximal correlation through

0≤ρ(1),ρ(1)2≤∥K2∥.0\le\rho(1),\qquad \rho(1)^2\le\lVert K^2\rVert.

For every measurable event AA, the power moments of its centered indicator are exactly the stationary event correlations:

⟨Km(1A−πA),1A−πA⟩=∫(1A(x)−πA)(Pm(x,A)−πA) π(dx).\langle K^m(1_A-\pi A),1_A-\pi A\rangle =\int (1_A(x)-\pi A)(P^m(x,A)-\pi A)\,\pi(dx).

The operator can be constructed from the coordinate-00 and coordinate-11 isometric embeddings into the path-space L2L^2 space and their Hilbert adjoints; the Markov property gives the power identity, while reversibility gives self-adjointness.

Preamble
import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure
import Definitions.Def_MixingCoefficients
import Definitions.Def_MarkovChainCLT_centeredIndicatorLp
import Mathlib.Analysis.InnerProductSpace.Adjoint

open MeasureTheory ProbabilityTheory Filter Set
open scoped ENNReal NNReal Topology ProbabilityTheory
open MarkovChainCLT
Formal statement
theorem MarkovChainCLT.stationary_reversible_centered_L2_operator
    {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P]
    (pi : Measure X) [IsProbabilityMeasure pi]
    (hinv : Kernel.Invariant P pi)
    (hrev : Kernel.IsReversible P pi) :
    ∃ K : Lp ℝ 2 pi →L[ℝ] Lp ℝ 2 pi,
      (K : Lp ℝ 2 pi →ₗ[ℝ] Lp ℝ 2 pi).IsSymmetric ∧
      K (Lp.const 2 pi (1 : ℝ)) = 0 ∧
      0 ≤ rhoMixingCoef (chainMeasure P pi) (fun i omega => omega i) 1 ∧
      (rhoMixingCoef (chainMeasure P pi) (fun i omega => omega i) 1) ^ 2 ≤ ‖K ^ 2‖ ∧
      ∀ (A : Set X) (hA : MeasurableSet A) (m : ℕ),
        inner ℝ ((K ^ m) (centeredIndicatorLp pi A hA))
            (centeredIndicatorLp pi A hA) =
          ∫ x,
            ((A.indicator (fun _ => (1 : ℝ))) x - pi.real A) *
              (((iterKernel P m) x A).toReal - pi.real A) ∂pi := by sorry
Source
G. O. Roberts and J. S. Rosenthal, Geometric Ergodicity and Hybrid Markov Chains, Electronic Communications in Probability 2 (1997), proof of Theorem 2, 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