Martingale CLT for the martingale differences of a stationary chain

Proved

MarkovChainCLT.martingaleCLT_chain

by LukeBernese · Aug 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

central-limit-theoremmarkov-chainsmartingaleprobability

Let $X$ be a Harris ergodic Markov chain run from its invariant distribution $\pi$ , and let $g \in L^2(\pi)$ . Set

D_i \;=\; g(X_{i+1}) - (Pg)(X_i), \qquad (Pg)(x) = \int g(y)\,P(x,\mathrm{d}y).

Then $\{D_i\}$ is a square-integrable martingale difference sequence for the natural filtration — $E[g(X_{i+1}) \mid X_0,\dots,X_i] = (Pg)(X_i)$ is precisely the Markov property — and it is stationary and ergodic because the chain is. The martingale central limit theorem then gives an asymptotic variance $v \ge 0$ with

\frac{1}{\sqrt n}\sum_{i<n} D_i \;\xrightarrow{d}\; N(0, v),

and $v = E[D_0^2]$ .

This is the central limit theorem of Billingsley (1961) and Ibragimov (1963) for stationary ergodic square-integrable martingale differences, specialised to the differences generated by a Markov chain so that the filtration and the increments are explicit. Stationarity supplies the conditional Lindeberg condition automatically: the conditional variances $E[D_i^2 \mid \mathcal{F}_{i-1}]$ form a stationary ergodic sequence, so their Cesàro averages converge a.s. to $E[D_0^2]$ by the ergodic theorem, and the truncation term vanishes because $D_0 \in L^2$ .

It is the analytic core of the martingale-approximation route to the Markov chain CLT: combined with a solution of the Poisson equation and Slutsky's theorem it yields the central limit theorem for $\sqrt n(\bar f_n - E_\pi f)$ without passing through mixing coefficients at all.

Preamble

import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.martingaleCLT_chain {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (g : X → ℝ) (hg : Measurable g) (hgL2 : MemLp g 2 π) :
    ∃ v : ℝ≥0, TendstoInDistribution
      (fun (n : ℕ) (ω : ℕ → X) =>
        (Real.sqrt n)⁻¹ * ∑ i ∈ Finset.range n, (g (ω (i + 1)) - ∫ y, g y ∂(P (ω i))))
      atTop (id : ℝ → ℝ) (fun _ => chainMeasure P π) (gaussianReal 0 v) := by sorry

Source

L. Tierney, "Markov Chains for Exploring Posterior Distributions", Annals of Statistics 22 (1994) 1701-1728, Theorem 5 (the uniformly ergodic CLT); the martingale-approximation proof is M. I. Gordin (1969) / C. Kipnis and S. R. S. Varadhan, "Central limit theorem for additive functionals of reversible Markov processes", Comm. Math. Phys. 104 (1986) 1-19, Corollary 1.5. Cited as the route to Corollary 5 in G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Remark 8 and Section 4.

View graph