CLT under polynomial drift: $\Delta V \le -dV^\tau + b\,\mathbb{1}_C$ , $|f| \le V^{\tau+\eta-1}$ (Jones Thm 1(ii))

Open

MarkovChainCLT.clt_of_polynomial_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$ , $0 \le \tau < 1$ , the polynomial drift condition

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

holds with $V$ integrable under every $P(x, \cdot)$ , and $\eta$ satisfies $1 - \tau \le \eta \le 1$ together with $E_\pi V^{2\eta} < \infty$ and $|f| \le V^{\tau + \eta - 1}$ 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 extends the drift route to chains converging only at a polynomial rate (Jarner–Roberts, Theorem 4.2), the regime of many heavy-tailed MCMC samplers.

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 2** (Jarner–Roberts 2002, Theorem 4.2): a Harris ergodic
chain satisfying the polynomial drift condition towards a small set, with
`|f| ≤ V^{τ+η-1}` for some `1 - τ ≤ η ≤ 1` such that `E_π V^{2η} < ∞`,
satisfies the CLT for every initial distribution. -/

Formal statement

theorem MarkovChainCLT.clt_of_polynomial_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) (hτ0 : 0 ≤ τ) (hτ1 : τ < 1)
    (hdrift : PolyDriftCondition P V d b τ C)
    (η : ℝ) (hη0 : 1 - τ ≤ η) (hη1 : η ≤ 1)
    (hVint : Integrable (fun x => V x ^ (2 * η)) π)
    (hfV : ∀ x, |f x| ≤ V x ^ (τ + η - 1)) :
    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 2 (arXiv v2 p. 4, eq. (6) drift); original: S. F. Jarner & G. O. Roberts, Polynomial convergence rates of Markov chains, Ann. Appl. Probab. 12 (2002), Theorem 4.2

Read-back

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

Let $X$ be a type carrying a countably generated σ-algebra (MeasurableSpace.CountablyGenerated: generated by some countable family of sets), $P$ a Markov kernel from $X$ to itself (each $P(x,\cdot)$ a probability measure), and $\pi$ a probability measure on $X$ . Hypotheses: (i) Harris ergodicity: $\pi$ is invariant for $P$ , and for every $x\in X$ , $\operatorname{tv}(P^n(x,\cdot),\pi)\to 0$ , where $P^n$ is the $n$ -fold iterate ( $P^0$ = identity) and $\operatorname{tv}(\mu,\nu)=\sup\{|\mu(A)-\nu(A)| : A\text{ measurable}\}$ (real supremum over measure values converted to reals; no factor $\tfrac12$ ); (ii) $f:X\to\mathbb{R}$ measurable; (iii) $V:X\to\mathbb{R}$ measurable with $V(x)\ge 1$ for all $x$ ; (iv) $C$ a measurable small set: $\exists\,n_0\ge 1$ , $\varepsilon>0$ , and a probability measure $Q$ with $\varepsilon\,Q(A)\le P^{n_0}(x,A)$ for all $x\in C$ and measurable $A$ (vacuous if $C=\emptyset$ ); (v) reals $d,b,\tau$ with $d>0$ , $0\le\tau<1$ ( $b$ unrestricted in sign) satisfying the polynomial drift condition: $V$ is integrable under $P(x,\cdot)$ for every $x$ , and for every $x$ , $\int V\,dP(x,\cdot)-V(x)\ \le\ -d\,V(x)^{\tau}+b\,\mathbf 1_C(x)$ , where $V(x)^{\tau}$ is the real-exponent power (with $V\ge1$ this is the usual power; when $\tau=0$ it is identically $1$ , making the drift bound $-d+b\,\mathbf 1_C(x)$ ); (vi) a real $\eta$ with $1-\tau\le\eta\le 1$ ; (vii) the function $x\mapsto V(x)^{2\eta}$ (real-exponent power) is integrable with respect to $\pi$ (Integrable: a.e. strongly measurable and $\int |V^{2\eta}|\,d\pi<\infty$ ); (viii) $|f(x)|\le V(x)^{\tau+\eta-1}$ for every $x$ — under the stated constraints the exponent $\tau+\eta-1$ lies in $[0,\tau]$ , and in the boundary case $\eta=1-\tau$ it is $0$ , so this hypothesis then reads $|f|\le 1$ . Conclusion (SatisfiesCLT): there exists $v\ge 0$ (a nonnegative real) such that for every initial probability distribution $\lambda$ on $X$ , the functions $Z_n(\omega)=\sqrt{n}\big(\tfrac1n\sum_{i=1}^{n}f(\omega_i)-\int f\,d\pi\big)$ converge in distribution as $n\to\infty$ , under the Ionescu–Tulcea path measure of the chain with $\omega_0\sim\lambda$ and $\omega_{n+1}\sim P(\omega_n,\cdot)$ , to gaussianReal 0 v — the mean- $0$ normal law with variance $v$ , equal to the point mass at $0$ when $v=0$ (so a degenerate limit satisfies the conclusion). TendstoInDistribution here asserts weak convergence of the pushforward laws of $Z_n$ to $\mathcal N(0,v)$ . Note: the average uses coordinates $1,\dots,n$ (coordinate $0$ excluded; the $n=0$ term is $0$ via $0^{-1}=0$ ), and a single $v$ must serve all initial laws $\lambda$ (existential before universal).

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 polynomial drift: ΔV≤−dVτ+b 1C\Delta V \le -dV^\tau + b\,\mathbb{1}_CΔV≤−dVτ+b1C​, ∣f∣≤Vτ+η−1|f| \le V^{\tau+\eta-1}∣f∣≤Vτ+η−1 (Jones Thm 1(ii))

CLT under polynomial drift: $\Delta V \le -dV^\tau + b\,\mathbb{1}_C$ , $|f| \le V^{\tau+\eta-1}$ (Jones Thm 1(ii))