Prove2Me

Distributional limit for an exponentially strongly mixing sequence with a Y2log⁡+∣Y∣Y^2\log^+|Y| moment

Proved
MarkovChainCLT.tendstoInDistribution_of_exp_alpha_of_log_moment

by evgeth · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

central-limit-theoremmixing-processesprobability

Let Y=(Yn)n≥0Y=(Y_n)_{n\ge 0} be a measurable, centered, strictly stationary real-valued sequence on a probability space (Ω,F,P)(\Omega,\mathcal F,P) with exponentially decaying strong mixing coefficients, α(n)≤c an\alpha(n)\le c\,a^n for some 0≤a<10\le a<1, and with E[Y02log⁡+∣Y0∣]<∞E[Y_0^2\log^+|Y_0|]<\infty. Assume also that the positive-lag autocovariance series ∑k≥1E[Y0Yk]\sum_{k\ge 1}E[Y_0Y_k] is absolutely convergent, and define

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

If σ2>0\sigma^2>0, then the normalized partial sums obey

1n∑i=0n−1Yi→dN(0,σ2).\frac{1}{\sqrt n}\sum_{i=0}^{n-1}Y_i\xrightarrow{d}N(0,\sigma^2).

This isolates the blocking and distributional-limit component of the Doukhan–Massart–Rio central limit theorem (Jones, Theorem 6), after covariance convergence has been established separately.

Formalization Note Convergence is weak convergence of the laws under the common probability measure PP; the Gaussian variance is represented by the nonnegative-real coercion of σ2\sigma^2, which equals σ2\sigma^2 under the positivity hypothesis.

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
Formal statement
/-- The blocking/limit component of the Doukhan–Massart–Rio CLT, after covariance
summability has been isolated. -/
theorem MarkovChainCLT.tendstoInDistribution_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)
    (hsum : Summable (fun k : ℕ => ∫ ω, Y 0 ω * Y (k + 1) ω ∂P))
    (hvar : 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, https://arxiv.org/abs/math/0409112, Theorem 6 (arXiv v2 p. 11); original: P. Doukhan, P. Massart and E. Rio, The functional central limit theorem for strongly mixing processes, Ann. Inst. H. Poincaré Probab. Statist. 30 (1994) 63-82 (special case)

View graph