Prove2Me

Centered-indicator power decay extends to a dense L2L^2 core

Proved
MarkovChainCLT.centered_indicator_decay_extends_to_dense_L2_core

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

dense-subspacel2simple-functionsspectral-decay

Let KK be a self-adjoint bounded operator on real L2(π)L^2(\pi) which annihilates constants. Suppose every centered event indicator has the uniform even-power estimate

∣⟨K2n(1A−πA),1A−πA⟩∣≤Ct2n(n≥1).|\langle K^{2n}(1_A-\pi A),1_A-\pi A\rangle|\le C t^{2n}\qquad(n\ge1).

Then there is a dense linear core DD (the integrable simple functions) such that each z∈Dz\in D has a constant Cz≥0C_z\ge0 with

∣⟨(K2)nz,z⟩∣≤Cz(t2)n(n≥0).|\langle (K^2)^n z,z\rangle|\le C_z(t^2)^n\qquad(n\ge0).

The proof decomposes simple functions over finitely many disjoint measurable atoms. Centering removes their constant component, and polarization plus the indicator estimate controls all finitely many cross terms. Density is the standard density of simple functions in L2L^2.

Preamble
import Definitions.Def_MarkovChainCLT_centeredIndicatorLp
import Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
import Mathlib.MeasureTheory.Function.L2Space
import Mathlib.Analysis.InnerProductSpace.Adjoint

open MeasureTheory Filter Set
open scoped ENNReal NNReal Topology
open MarkovChainCLT
Formal statement
theorem MarkovChainCLT.centered_indicator_decay_extends_to_dense_L2_core
    {X : Type*} [MeasurableSpace X]
    (pi : Measure X) [IsProbabilityMeasure pi]
    (K : Lp ℝ 2 pi →L[ℝ] Lp ℝ 2 pi)
    (hKsym : (K : Lp ℝ 2 pi →ₗ[ℝ] Lp ℝ 2 pi).IsSymmetric)
    (hKone : K (Lp.const 2 pi (1 : ℝ)) = 0)
    (t C : ℝ) (ht : 0 ≤ t) (hC : 0 ≤ C)
    (hdiag : ∀ (A : Set X) (hA : MeasurableSet A) (n : ℕ), 1 ≤ n →
      |inner ℝ ((K ^ (2 * n)) (centeredIndicatorLp pi A hA))
        (centeredIndicatorLp pi A hA)| ≤ C * t ^ (2 * n)) :
    ∃ D : Submodule ℝ (Lp ℝ 2 pi), Dense (D : Set (Lp ℝ 2 pi)) ∧
      ∀ z : D, ∃ Cz : ℝ, 0 ≤ Cz ∧
        ∀ n : ℕ, |inner ℝ (((K ^ 2) ^ 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), proof of Theorem 2, pp. 7-9, https://www.probability.ca/jeff/ftpdir/hybrid.pdf; the dense-simple-function and polarization step is the standard extension of the displayed-set calculation in that proof.

View graph