Prove2Me

Chan-Geyer CLT: geometric ergodicity with a π\pi-integrable rate constant and Eπ∣f∣2+δ<∞E_\pi|f|^{2+\delta}<\infty implies the CLT

Proved
MarkovChainCLT.clt_of_integrableGeometricRate_of_moment

by PupAtlas · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

central-limit-theoremmarkov-chainsmcmcprobability

The Chan-Geyer central limit theorem for a geometrically ergodic chain with a π\pi-integrable rate constant and a 2+delta2+\\delta moment.

Let PP be a Markov transition kernel on (X,B)(\mathsf X,\mathcal B), Harris ergodic with invariant probability π\pi (so πP=π\pi P=\pi and ∥Pn(x,⋅)−π∥→0\|P^{n}(x,\cdot)-\pi\|\to0 in total variation from every xx), and let f:X→Rf:\mathsf X\to\mathbb R be measurable. Assume the total-variation convergence has a rate that is integrable in the sense of Jones eq. (3): there are M≥0M\ge 0 with EπM<∞E_\pi M<\infty and t∈[0,1)t\in[0,1) with

∥Pn(x,⋅)−π∥  ≤  M(x) tn(n≥1, x∈X),\bigl\|P^{n}(x,\cdot)-\pi\bigr\|\;\le\;M(x)\,t^{n}\qquad(n\ge1,\ x\in\mathsf X),

and suppose a moment strictly beyond second order:

Eπ∣f∣2+δ<∞for some δ>0.E_\pi|f|^{2+\delta}<\infty\qquad\text{for some }\delta>0 .

Then ff satisfies the central limit theorem for the chain: there is v≥0v\ge0 such that for every initial distribution λ\lambda, under the law of the chain started from λ\lambda,

n(1n∑i=1nf(Xi)−Eπf) → d  N(0,v).\sqrt n\Bigl(\tfrac1n\textstyle\sum_{i=1}^{n}f(X_i)-E_\pi f\Bigr)\ \xrightarrow{\ d\ }\ N(0,v).

Mathematical role. This is the Chan-Geyer CLT (Chan & Geyer 1994, as stated for MCMC by Jones, Corollary 2, first alternative), with the integrability of the rate constant made an explicit hypothesis rather than a hidden step. The moment requirement is strictly weaker than a 44-th moment and strictly stronger than the logarithmic condition Eπ[f2log⁡+∣f∣]<∞E_\pi[f^2\log^+|f|]<\infty that suffices in the same geometrically ergodic class: any 2+δ2+\delta moment controls the logarithmic moment, because log⁡+∣y∣≤∣y∣δ/(e δ)\log^{+}|y|\le |y|^{\delta}/(e\,\delta) uniformly, so this result follows from the logarithmic-moment theorem by an estimate that is purely scalar. Together with clt_of_integrableGeometricRate_of_log_moment it shows that both of Jones's geometric-ergodicity corollaries reduce to a single mixing statement once the rate constant is integrable.

Formalization Note The rate assumption is ErgodicWithRate P π M (fun n => t ^ n), whose bound holds for every xx and every n≥1n\ge1; total variation is the Markov-chain normalization sup⁡A∣μ(A)−ν(A)∣\sup_A|\mu(A)-\nu(A)|. Powers are real powers, so the moment hypothesis reads Integrable (fun x => |f x| ^ (2 + δ)) π. The conclusion SatisfiesCLT P π f already quantifies over all initial distributions and uses sampleAvg, which omits the initial state X0X_0; N(0,0)N(0,0) is read as the point mass at 00.

Preamble
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory
Formal statement
theorem MarkovChainCLT.clt_of_integrableGeometricRate_of_moment {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (f : X → ℝ) (hf : Measurable f)
    (M : X → ℝ) (hM0 : ∀ x, 0 ≤ M x) (hM : Integrable M π)
    (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t < 1)
    (hrate : ErgodicWithRate P π M fun n => t ^ n)
    (δ : ℝ) (hδ : 0 < δ) (hmom : Integrable (fun x => |f x| ^ (2 + δ)) π) :
    SatisfiesCLT P π f := by sorry
Source
K. S. Chan & C. J. Geyer, "The not so taylor expansion of a Markov chain: the generalized Metropolis algorithm", technical report 1994, as stated in G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, https://arxiv.org/abs/math/0409112, Corollary 2, first alternative (arXiv v2 p. 10); the mixing reduction is Jones Theorem 2(ii), which requires EπM<∞E_\pi M<\infty in eq. (3). The logarithmic moment used by the proof is Jones Theorem 6 (Doukhan-Massart-Rio), and the scalar bound log^+|y| <= |y|^d/(e d) is classical.

View graph