Prove2Me

Doukhan–Massart–Rio CLT: α(n)=O(an)\alpha(n) = O(a^n), E[Y2log⁡+∣Y∣]<∞E[Y^2\log^+|Y|] < \infty (Jones Thm 6)

Proved
MarkovChainCLT.clt_of_exp_alpha_of_log_moment

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

central-limit-theoremmixing-processesprobability

Let Y={Yn}n≥0Y = \{Y_n\}_{n \ge 0} be a centered, strictly stationary sequence of real random variables on a probability space, with partial sums Sn=∑i<nYiS_n = \sum_{i < n} Y_i. Suppose the strong mixing coefficients decay exponentially, α(n)≤c an\alpha(n) \le c\, a^n for some 0≤a<10 \le a < 1, and

E[Y02 log⁡+∣Y0∣]<∞,log⁡+t=max⁡(0,log⁡t).E\bigl[Y_0^2 \, \log^+ |Y_0|\bigr] < \infty, \qquad \log^+ t = \max(0, \log t).

Then the series

σ2  =  E[Y02]  +  2∑k≥1E[Y0Yk]\sigma^2 \;=\; E[Y_0^2] \;+\; 2 \sum_{k \ge 1} E[Y_0 Y_k]

converges absolutely, and if σ2>0\sigma^2 > 0 then Sn/n→dN(0,σ2)S_n / \sqrt{n} \xrightarrow{d} N(0, \sigma^2) as n→∞n \to \infty.

This Doukhan–Massart–Rio theorem trades the 2+δ2+\delta moment for a barely-more-than-second moment when mixing is exponentially fast — the sharpest sequence-level input available for geometrically ergodic chains.

Formalization Note The stated moment already implies E[Y02]<∞E[Y_0^2] < \infty, so square-integrability is not assumed separately. Sequences are indexed from 00, so Sn=Y0+⋯+Yn−1S_n = Y_0 + \cdots + Y_{n-1} and the past σ\sigma-algebras used by the mixing coefficients start at Y0Y_0; under strict stationarity this agrees with the source, which indexes from 11. Absolute convergence of the covariance series is expressed as unconditional summability, and the limit statement is weak convergence of the laws of Sn/nS_n/\sqrt{n}.

Preamble
import Definitions.Def_MixingCoefficients
import Mathlib.MeasureTheory.Function.ConvergenceInDistribution
import Mathlib.Probability.Distributions.Gaussian.Real
import Mathlib.Analysis.SpecialFunctions.Log.PosLog

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

/-- **Theorem 6** (Doukhan–Massart–Rio 1994): a centered strictly stationary
sequence with exponentially fast strong mixing and `E[Y₀² log⁺|Y₀|] < ∞` satisfies
`σ² = E[Y₀²] + 2 ∑_{k≥1} E[Y₀ Y_k]` (absolutely convergent), and if `σ² > 0` then
`S_n / √n →d N(0, σ²)`. -/
Formal statement
theorem MarkovChainCLT.clt_of_exp_alpha_of_log_moment {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : ℕ → Ω → ℝ)
    (hY : ∀ n, Measurable (Y n)) (hstat : IsStrictlyStationary P Y)
    (hcent : ∫ ω, Y 0 ω ∂P = 0)
    (c a : ℝ) (ha0 : 0 ≤ a) (ha1 : a < 1)
    (hα : ∀ n, alphaMixingCoef P Y n ≤ c * a ^ n)
    (hmom : Integrable (fun ω => (Y 0 ω) ^ 2 * Real.posLog |Y 0 ω|) P) :
    Summable (fun k : ℕ => ∫ ω, Y 0 ω * Y (k + 1) ω ∂P) ∧
      (0 < seqAsymptoticVariance P Y →
        TendstoInDistribution
          (fun (n : ℕ) ω => (Real.sqrt n)⁻¹ * ∑ i ∈ Finset.range n, Y i ω)
          atTop (id : ℝ → ℝ) (fun _ => P)
          (gaussianReal 0 (seqAsymptoticVariance P Y).toNNReal)) := by sorry
Source
G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Theorem 6 (arXiv v2 p. 11); original: P. Doukhan, P. Massart & E. Rio, Ann. Inst. H. Poincare Probab. Statist. 30 (1994) (special case)

View graph