Centered event indicator in real $L^2$

Definition

MarkovChainCLT_centeredIndicatorLp

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

centeringindicatorl2markov-chain

For a probability measure $\pi$ and a measurable event $A$ , centeredIndicatorLp pi A hA is the real $L^2(\pi)$ equivalence class of $1_A-\pi(A)$ . It is the standard dense-core generator used in the spectral analysis of stationary Markov operators.

Definition code

import Mathlib.MeasureTheory.Function.LpSpace.Indicator

open MeasureTheory

namespace MarkovChainCLT

/-- The centered indicator of a measurable set, viewed as an element of real `L²`. -/
noncomputable def centeredIndicatorLp
    {X : Type*} [MeasurableSpace X]
    (pi : Measure X) [IsProbabilityMeasure pi]
    (A : Set X) (hA : MeasurableSet A) : Lp ℝ 2 pi :=
  indicatorConstLp 2 hA (measure_ne_top pi A) (1 : ℝ) -
    Lp.const 2 pi (pi.real A)

end MarkovChainCLT

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.

View graph

Centered event indicator in real L2L^2L2

Centered event indicator in real $L^2$