Prove2Me

Jones's Corollary 3 with a π\pi-integrable geometric rate constant: Eπ[f2log⁡+∣f∣]<∞E_\pi[f^2\log^+|f|]<\infty implies the CLT

Proved
MarkovChainCLT.clt_of_integrableGeometricRate_of_log_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.

Let PP be a Markov transition kernel on a measurable space (X,B)(\mathsf X,\mathcal B), Harris ergodic with invariant probability distribution π\pi — meaning π\pi is invariant and ∥Pn(x,⋅)−π∥→0\|P^{n}(x,\cdot)-\pi\|\to0 in total variation from every starting point xx — and let f:X→Rf:\mathsf X\to\mathbb R be measurable. Suppose the convergence comes with 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) such that

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

and suppose moreover the logarithmic moment condition

Eπ[f2log⁡+∣f∣]<∞,log⁡+u=max⁡(0,log⁡u).E_\pi\bigl[f^{2}\log^{+}|f|\bigr]<\infty,\qquad \log^{+}u=\max(0,\log u).

Then ff satisfies the central limit theorem for the chain: there is v≥0v\ge 0 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).

Why the rate constant must be integrable. This is Jones's Corollary 3 with the hypothesis that its proof actually consumes. The route of record — Theorem 6 applied to the chain, fed by Theorem 2(ii) — needs a bound on the strong mixing coefficients of the form α(n)≤γ(n)EπM\alpha(n)\le \gamma(n)E_\pi M, and that inequality is derived from eq. (3) only when MM is π\pi-integrable. Geometric ergodicity as defined in Def_MarkovErgodicity provides a finite pointwise constant, not an integrable one: the countdown chain on the countable–cocountable space exhibits geometric ergodicity with no π\pi-integrable rate constant at all. Making EπM<∞E_\pi M<\infty a hypothesis rather than a lemma isolates exactly the missing ingredient; compare PolynomiallyErgodicL1, which already requires Integrable M π in its own definition, so that the geometric case is the only asymmetric one.

Formalization Note The rate assumption is stated as ErgodicWithRate P π M (fun n => t ^ n), whose bound quantifies over all xx and all n≥1n\ge1; total variation uses the Markov-chain normalization sup⁡A∣μ(A)−ν(A)∣\sup_A|\mu(A)-\nu(A)| of Def_TotalVariationDist. The conclusion is the property SatisfiesCLT P π f, which already ranges over all initial distributions, with sampleAvg omitting the initial point X0X_0, and N(0,0)N(0,0) read as the point mass at 00.

Preamble
import Mathlib.Analysis.SpecialFunctions.Log.PosLog
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_log_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)
    (hmom : Integrable (fun x => f x ^ 2 * Real.posLog |f x|) π) :
    SatisfiesCLT P π f := by sorry
Source
G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, https://arxiv.org/abs/math/0409112, Corollary 3 (arXiv v2 p. 11), proved there from Theorem 6 via Theorem 2(ii); the integrability of the rate constant is the standing hypothesis of Theorem 2(ii) ("if (3) holds with EπM<∞E_\pi M<\infty ... then α(n)≤γ(n)EπM\alpha(n)\le \gamma(n)E_\pi M", arXiv v2 p. 7). Geometric ergodicity itself is defined in Jones section 2 by eq. (3) with no integrability, which is why the hypothesis appears here explicitly.

View graph