Chan–Geyer and polynomial-ergodicity CLTs (Jones Cor 2)

Open

MarkovChainCLT.clt_of_geometric_or_polynomial

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$ . Assume one of the following three conditions: (1) the chain is geometrically ergodic and $E_\pi |f|^{2+\delta} < \infty$ for some $\delta > 0$ ; (2) the chain is polynomially ergodic of order $m$ with $E_\pi M < \infty$ for the rate constant $M$ , and $E_\pi |f|^{2+\delta} < \infty$ for some $\delta > 0$ with $m\delta > 2 + \delta$ ; (3) the chain is polynomially ergodic of order $m > 1$ with $E_\pi M < \infty$ , and $|f| < B$ $\pi$ -almost surely for some $B$ .

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).

Case (1) is the Chan–Geyer CLT, the most frequently cited sufficient condition in the MCMC literature; cases (2)–(3) are its polynomial analogues.

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 2** (case 1: Chan–Geyer 1994): a Harris ergodic chain satisfying one
of: (1) geometric ergodicity with `E_π |f|^{2+δ} < ∞` for some `δ > 0`;
(2) polynomial ergodicity of order `m` with integrable constant and
`E_π |f|^{2+δ} < ∞` with `mδ > 2+δ`; (3) polynomial ergodicity of order `m > 1`
with integrable constant and `f` bounded `π`-a.s. — satisfies the CLT for every
initial distribution. -/

Formal statement

theorem MarkovChainCLT.clt_of_geometric_or_polynomial {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (f : X → ℝ) (hf : Measurable f)
    (hcase :
      (GeometricallyErgodic P π ∧
        ∃ δ : ℝ, 0 < δ ∧ Integrable (fun x => |f x| ^ (2 + δ)) π) ∨
      (∃ m δ : ℝ, 0 < δ ∧ 2 + δ < m * δ ∧ PolynomiallyErgodicL1 P π m ∧
        Integrable (fun x => |f x| ^ (2 + δ)) π) ∨
      (∃ m : ℝ, 1 < m ∧ PolynomiallyErgodicL1 P π m ∧
        ∃ B : ℝ, ∀ᵐ x ∂π, |f x| < B)) :
    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 2 (arXiv v2 p. 10); case 1: K. S. Chan & C. J. Geyer, Ann. Statist. 22 (1994), discussion of Tierney

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, junk value $0$ if unbounded, and the set contains $0$ via $A = \varnothing$ ). (2) $f : X \to \mathbb R$ is measurable. (3) A three-way disjunction — at least one of the following holds: (A) [geometric case] $P$ is geometrically ergodic for $\pi$ : there exist $M : X \to \mathbb R$ and $t \in \mathbb R$ with $M(x) \ge 0$ for all $x$ (no measurability or integrability of $M$ is required), $0 \le t < 1$ , and $d_{TV}(P^n(x,\cdot),\pi) \le M(x)\, t^n$ for every $x$ and every $n \ge 1$ ( $t^n$ is the ordinary natural-number power; nothing is asserted at $n=0$ ); and there exists a real $\delta > 0$ such that $x \mapsto |f(x)|^{2+\delta}$ is integrable with respect to $\pi$ (real-exponent power of the nonnegative base, $0^{2+\delta}=0$ ). (B) [polynomial case with moment] there exist reals $m, \delta$ with $0 < \delta$ , $2 + \delta < m\,\delta$ , such that $P$ is polynomially ergodic in the $L^1$ sense with exponent $m$ : there exists $M : X \to \mathbb R$ , pointwise nonnegative and integrable with respect to $\pi$ , with $d_{TV}(P^n(x,\cdot),\pi) \le M(x)\, n^{-m}$ for every $x$ and every $n \ge 1$ (here $n^{-m}$ is the real number $n$ raised to the real exponent $-m$ ; only $n \ge 1$ is constrained); and $x \mapsto |f(x)|^{2+\delta}$ is integrable with respect to $\pi$ . (C) [polynomial case with bounded $f$ ] there exists a real $m$ with $1 < m$ such that $P$ is polynomially ergodic in the $L^1$ sense with exponent $m$ (same unfolding as in (B)); and there exists a real $B$ (with no positivity constraint stated) such that $|f(x)| < B$ strictly for $\pi$ -almost every $x$ . 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$ , $0^{-1}=0$ and $\sqrt 0 = 0$ give $Z_0=0$ ); $\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$ ; 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