CLT under geometric drift: $\Delta V \le -dV + b\,\mathbb{1}_C$ , $f^2 \le V$ (Jones Thm 1(i))

Open

MarkovChainCLT.clt_of_geometric_drift

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 $V : \mathsf{X} \to [1, \infty)$ is measurable, $C$ is a measurable small set, $d > 0$ and $b$ are constants, the geometric drift condition

PV(x) - V(x) \;\le\; -d\, V(x) + b\, \mathbb{1}_C(x) \qquad (x \in \mathsf{X})

holds with $V$ integrable under every $P(x, \cdot)$ , and $f^2 \le V$ pointwise.

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

This is the workhorse CLT of applied Markov chain Monte Carlo: drift towards a small set is the standard checkable route to a CLT for a specific sampler (Meyn–Tweedie, Theorem 17.0.1).

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. The $\sigma$ -algebra of the state space is additionally assumed countably generated, the standard general-state-space setting of Meyn and Tweedie.

Preamble

import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovDriftMinorization
import Definitions.Def_MarkovChainPathMeasure

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

/-- **Theorem 1, condition 1** (Meyn–Tweedie 1993, Theorem 17.0.1): a Harris ergodic
chain satisfying the geometric drift condition towards a small set, with
`f² ≤ V`, satisfies the CLT for every initial distribution. -/

Formal statement

theorem MarkovChainCLT.clt_of_geometric_drift {X : Type*} [MeasurableSpace X]
    [MeasurableSpace.CountablyGenerated X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (f : X → ℝ) (hf : Measurable f)
    (V : X → ℝ) (hV : Measurable V) (hV1 : ∀ x, 1 ≤ V x)
    (C : Set X) (hC : MeasurableSet C) (hsmall : IsSmallSet P C)
    (d b : ℝ) (hd : 0 < d) (hdrift : GeoDriftCondition P V d b C)
    (hfV : ∀ x, f x ^ 2 ≤ V x) :
    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, Theorem 1, condition 1 (arXiv v2 p. 4, eq. (5) drift); original: S. P. Meyn & R. L. Tweedie, Markov Chains and Stochastic Stability (1993), Theorem 17.0.1

Read-back

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

Let $X$ be a type carrying a σ-algebra assumed countably generated (MeasurableSpace.CountablyGenerated: the σ-algebra is generated by some countable family of sets). Let $P$ be a Markov kernel from $X$ to itself (each $P(x,\cdot)$ is a probability measure on $X$ ) and $\pi$ a probability measure on $X$ . The hypotheses are: (i) Harris ergodicity of $(P,\pi)$ , unfolded as the conjunction of ( $\pi$ is invariant for $P$ ) and (for every starting point $x\in X$ , $\operatorname{tv}(P^n(x,\cdot),\pi)\to 0$ as $n\to\infty$ ), where $P^n$ denotes the $n$ -fold kernel iterate ( $P^0$ = identity kernel, $P^{n+1}=P\circ P^n$ ) and $\operatorname{tv}(\mu,\nu)$ is the bundle's custom total-variation distance $\sup\{\,|\mu(A)-\nu(A)|\ :\ A\ \text{measurable}\,\}$ — a real-valued supremum taken over measure values converted to real numbers (infinite measure values become $0$ ), with no factor $\tfrac12$ ; (ii) $f:X\to\mathbb{R}$ is measurable; (iii) $V:X\to\mathbb{R}$ is measurable with $V(x)\ge 1$ for every $x$ ; (iv) $C\subseteq X$ is a measurable set that is small for $P$ , unfolded as: there exist an integer $n_0\ge 1$ , a real $\varepsilon>0$ , and a probability measure $Q$ on $X$ such that $\varepsilon\,Q(A)\le P^{n_0}(x,A)$ for every $x\in C$ and every measurable $A$ (an inequality of extended-nonnegative-real measure values; this is vacuously true when $C=\emptyset$ ); (v) reals $d,b$ with $d>0$ (no upper bound on $d$ is imposed, and $b$ may be any real, including negative) satisfying the geometric drift condition: $V$ is integrable under $P(x,\cdot)$ for every $x$ (integrable = a.e. strongly measurable with finite integral of the absolute value), and for every $x$ , $\int V\,dP(x,\cdot)-V(x)\ \le\ -d\,V(x)+b\,\mathbf 1_C(x)$ ; (vi) $f(x)^2\le V(x)$ for every $x$ . The conclusion is the bundle's SatisfiesCLT predicate: there exists a nonnegative real $v\ge 0$ such that for every initial probability distribution $\lambda$ on $X$ , the sequence of functions on path space $Z_n(\omega)=\sqrt{n}\Big(\tfrac1n\sum_{i=1}^{n}f(\omega_i)\ -\ \int f\,d\pi\Big)$ converges in distribution, along $n\to\infty$ and under the path measure of the chain started from $\lambda$ (the Ionescu–Tulcea measure on $\mathbb{N}\to X$ under which $\omega_0\sim\lambda$ and $\omega_{n+1}\sim P(\omega_n,\cdot)$ ), to gaussianReal 0 v, the normal law on $\mathbb{R}$ with mean $0$ and variance $v$ — which is the point mass at $0$ when $v=0$ , so the existential permits a degenerate limit. Here TendstoInDistribution (against the identity map on $\mathbb{R}$ carrying the law $\mathcal N(0,v)$ ) asserts that the pushforward laws of $Z_n$ converge weakly to $\mathcal N(0,v)$ . Points to note: the sample average runs over coordinates $1$ through $n$ and excludes the initial coordinate $\omega_0$ ; at $n=0$ the expression equals $0$ by Lean's convention $0^{-1}=0$ ; the quantifier order gives one single $v$ valid simultaneously for all initial laws $\lambda$ ; and the centering constant is the Bochner integral $\int f\,d\pi$ , which equals the junk value $0$ if $f$ is not $\pi$ -integrable (no integrability of $f$ or of $V$ with respect to $\pi$ is among the hypotheses).

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

CLT under geometric drift: ΔV≤−dV+b 1C\Delta V \le -dV + b\,\mathbb{1}_CΔV≤−dV+b1C​, f2≤Vf^2 \le Vf2≤V (Jones Thm 1(i))

CLT under geometric drift: $\Delta V \le -dV + b\,\mathbb{1}_C$ , $f^2 \le V$ (Jones Thm 1(i))