Roberts–Rosenthal CLT: geometric ergodicity + detailed balance + $E_\pi f^2 < \infty$ (Jones Cor 4)

Open

MarkovChainCLT.clt_of_geometric_reversible

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 geometrically ergodic, reversible with respect to $\pi$ (detailed balance, the source's eq. (8)), 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 Roberts–Rosenthal CLT: for reversible samplers — Metropolis–Hastings in particular — geometric ergodicity plus a second moment already gives the CLT, with no $\delta$ to spare.

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 4** (Roberts–Rosenthal 1997): a geometrically ergodic Harris chain
satisfying detailed balance, with `E_π f² < ∞`, satisfies the CLT for every initial
distribution. -/

Formal statement

theorem MarkovChainCLT.clt_of_geometric_reversible {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (f : X → ℝ) (hf : Measurable f)
    (hgeo : GeometricallyErgodic P π) (hrev : Kernel.IsReversible 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 4 (arXiv v2 p. 12; proved there from Theorem 7 via Theorem 2(iii)); original: G. O. Roberts & J. S. Rosenthal, Electron. Comm. Probab. 2 (1997), via Kipnis-Varadhan (1986), Corollary 1.5

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) Geometric ergodicity: 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$ 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$ (nothing asserted at $n=0$ ). (4) Reversibility (Kernel.IsReversible P \pi, a Mathlib notion): the joint law on $X \times X$ of a pair $(x,y)$ with $x \sim \pi$ and $y \sim P(x,\cdot)$ — the composition-product measure $\pi \otimes P$ — is invariant under swapping the two coordinates; i.e. detailed balance holds: $\pi(dx)\,P(x,dy)$ is a symmetric measure on $X \times X$ . (5) $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$ , $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

Roberts–Rosenthal CLT: geometric ergodicity + detailed balance + Eπf2<∞E_\pi f^2 < \inftyEπ​f2<∞ (Jones Cor 4)

Roberts–Rosenthal CLT: geometric ergodicity + detailed balance + $E_\pi f^2 < \infty$ (Jones Cor 4)