Prove2Me

Distributional limit for a summable-ρ\rho stationary sequence

Proved
MarkovChainCLT.tendstoInDistribution_of_summable_rho

by 98u6ygx9A7cbY8V · 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, with Y0∈L2Y_0\in L^2 and summable maximal-correlation coefficients. Assume also that its positive-lag autocovariance series is absolutely convergent. Define

σ2=E[Y02]+2∑k≥1E[Y0Yk].\sigma^2=\mathbb E[Y_0^2]+2\sum_{k\ge 1}\mathbb 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 summable-ρ\rho central limit theorem after covariance convergence has been established.

Formalization Note Convergence is weak convergence of the laws under the common probability measure; 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

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

/-- The blocking/limit component of the summable-rho CLT, after covariance
summability has been isolated. -/
Formal statement
theorem MarkovChainCLT.tendstoInDistribution_of_summable_rho
    {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : ℕ → Ω → ℝ)
    (hY : ∀ n, Measurable (Y n)) (hstat : IsStrictlyStationary P Y)
    (hcent : ∫ ω, Y 0 ω ∂P = 0) (hL2 : MemLp (Y 0) 2 P)
    (hρ : Summable (fun n => rhoMixingCoef P Y n))
    (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 7 and eq. (12), arXiv v2 p. 12; original result: I. A. Ibragimov, Theory of Probability and Its Applications 20 (1975).

View graph