Prove2Me

Ibragimov–Linnik CLT, moment case: E∣Y∣2+δ<∞E|Y|^{2+\delta} < \infty, ∑α(n)δ/(2+δ)<∞\sum \alpha(n)^{\delta/(2+\delta)} < \infty (Jones Thm 5(ii))

Proved
MarkovChainCLT.clt_of_moment_of_alpha_pow_summable

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 there is δ>0\delta > 0 with E∣Y0∣2+δ<∞E|Y_0|^{2+\delta} < \infty and

∑nα(n)δ/(2+δ)  <  ∞.\sum_{n} \alpha(n)^{\delta/(2+\delta)} \;<\; \infty.

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 is the moment case of the Ibragimov–Linnik central limit theorem (the source's eq. (10)), the engine behind the Chan–Geyer and polynomial-moment chain CLTs.

Formalization Note 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.Pow.Real

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

/-- **Theorem 5, condition 2** (Ibragimov 1962; Ibragimov–Linnik 1971): a centered
strictly stationary strongly mixing sequence with `E|Y₀|^{2+δ} < ∞` and
`∑_n α(n)^{δ/(2+δ)} < ∞` 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_moment_of_alpha_pow_summable {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : ℕ → Ω → ℝ)
    (hY : ∀ n, Measurable (Y n)) (hstat : IsStrictlyStationary P Y)
    (hcent : ∫ ω, Y 0 ω ∂P = 0)
    (δ : ℝ) (hδ : 0 < δ) (hmom : Integrable (fun ω => |Y 0 ω| ^ (2 + δ)) P)
    (hα : Summable (fun n => alphaMixingCoef P Y n ^ (δ / (2 + δ)))) :
    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 5, condition 2, eq. (10) (arXiv v2 p. 9); originals: I. A. Ibragimov (1962); Ibragimov & Linnik (1971), Theorem 18.5.3

View graph