Uniformly ergodic CLT: $E_\pi f^2 < \infty$ (Jones Cor 5)

Proved

MarkovChainCLT.clt_of_uniformly_ergodic

by Shuze Chen · Aug 15, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmcmcprobability

Let $X = \{X_n\}_{n \ge 0}$ be a Markov chain with transition kernel $P$ on a state space $\mathsf{X}$ , Harris ergodic with invariant probability distribution $\pi$ , and let $f : \mathsf{X} \to \mathbb{R}$ be measurable. Write $\bar f_n = n^{-1} \sum_{i=1}^{n} f(X_i)$ for the sample average and $E_\pi f = \int f \, d\pi$ . Suppose the chain is uniformly ergodic and

E_\pi f^2 < \infty.

Then the chain satisfies the central limit theorem for $f$ : there is a single asymptotic variance $\sigma_f^2 \ge 0$ such that for every initial distribution of the chain,

\sqrt{n}\,\bigl(\bar f_n - E_\pi f\bigr) \xrightarrow{d} N(0, \sigma_f^2) \qquad (n \to \infty).

The Tierney/Ibragimov–Linnik CLT for uniformly ergodic chains: under the strongest ergodicity condition, a second moment on the functional is all that is needed.

Formalization Note "Harris ergodic" is encoded by its total-variation characterization: $\pi$ is invariant for $P$ and $\|P^n(x, \cdot) - \pi\| \to 0$ for every starting point $x$ (equivalent to the classical aperiodic, $\psi$ -irreducible, positive Harris recurrent definition; the "every $x$ " quantifier is exactly the Harris property). Convergence in distribution is weak convergence of laws, and $N(0, 0)$ is read as the point mass at $0$ , which absorbs the source's " $\sigma_f^2 > 0$ " caveat.

Preamble

import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

/-- **Corollary 5** (Ibragimov–Linnik 1971; Tierney 1994): a uniformly ergodic
Harris chain with `E_π f² < ∞` satisfies the CLT for every initial distribution. -/

Formal statement

theorem MarkovChainCLT.clt_of_uniformly_ergodic {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (f : X → ℝ) (hf : Measurable f)
    (huni : UniformlyErgodic P π) (hL2 : MemLp f 2 π) :
    SatisfiesCLT P π f := by sorry

Source

G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Corollary 5 (arXiv v2 p. 13; proved there from Theorem 8 via Theorem 2(iv)); originals: Ibragimov & Linnik (1971); L. Tierney, Markov chains for exploring posterior distributions, Ann. Statist. 22 (1994)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Setting. $X$ is an arbitrary type with a measurable-space structure; $P$ is a kernel from $X$ to $X$ assumed (typeclass) to be a Markov kernel ( $P(x,\cdot)$ a probability measure for every $x$ ); $\pi$ is a measure on $X$ assumed (typeclass) to be a probability measure. Hypotheses. (1) Harris ergodicity: $\pi$ is invariant for $P$ ( $A \mapsto \int_X P(x,A)\,d\pi(x)$ equals $\pi$ ) and for every $x \in X$ , $d_{TV}(P^n(x,\cdot),\pi) \to 0$ as $n \to \infty$ , where $P^n$ is the $n$ -fold iterate ( $P^0 =$ identity kernel, $P^{n+1} = P \circ P^n$ ) and $d_{TV}(\mu,\nu) = \sup\{\,|\mu(A)-\nu(A)| : A \text{ measurable}\,\}$ (no factor $\tfrac12$ ; measure values sent to reals with $\infty \mapsto 0$ ; real supremum with junk value $0$ if unbounded, set contains $0$ via $A=\varnothing$ ). (2) $f : X \to \mathbb R$ is measurable. (3) Uniform ergodicity: there exist reals $R$ and $t$ with $R \ge 0$ , $0 \le t < 1$ , such that for every $x \in X$ and every $n \ge 1$ , $d_{TV}(P^n(x,\cdot),\pi) \le R\,t^n$ — the bounding constant $R$ is state-independent ( $t^n$ is the ordinary natural-number power; nothing is asserted at $n = 0$ ). (4) $f \in L^2(\pi)$ in the MemLp sense: $f$ is $\pi$ -a.e. strongly measurable and $\left(\int |f|^2\,d\pi\right)^{1/2} < \infty$ . Conclusion ( $f$ satisfies the CLT for $(P,\pi)$ , unfolded): there exists a nonnegative real $v$ such that for every probability measure $\lambda$ on $X$ — a single $v$ for all $\lambda$ ; existential over $v$ before universal over $\lambda$ — the functions $Z_n(\omega) = \sqrt{n}\,\left(\bar f_n(\omega) - \int_X f\,d\pi\right)$ converge in distribution to $\mathcal N(0,v)$ as $n \to \infty$ under the path measure $\mu_\lambda$ , where: $\bar f_n(\omega) = n^{-1}\sum_{i=0}^{n-1} f(\omega_{i+1})$ averages $f$ over the chain states at times $1,\dots,n$ (the time- $0$ state is never used; at $n=0$ , Lean's $0^{-1}=0$ and $\sqrt 0=0$ give $Z_0=0$ ); the centering constant is the $\pi$ -mean for every $\lambda$ ; $\mu_\lambda$ is the law on $\mathbb N \to X$ of the time-homogeneous Markov chain with transition kernel $P$ started with $\omega_0 \sim \lambda$ ( $\omega_{n+1} \sim P(\omega_n,\cdot)$ , Ionescu–Tulcea); convergence in distribution means $\int g(Z_n)\,d\mu_\lambda \to \int_{\mathbb R} g\,d\mathcal N(0,v)$ for every bounded continuous $g : \mathbb R \to \mathbb R$ ; and $\mathcal N(0,v)$ is the normal law of mean $0$ and variance $v$ , equal to the Dirac point mass at $0$ when $v=0$ (degenerate limit allowed).

Human review

Endorsed by Community (Bot) · Aug 15, 2026
Endorsed by Shuze Chen · Aug 15, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Uniformly ergodic CLT: Eπf2<∞E_\pi f^2 < \inftyEπ​f2<∞ (Jones Cor 5)

Uniformly ergodic CLT: $E_\pi f^2 < \infty$ (Jones Cor 5)