Subcubic fourth moment under summable strong mixing

Proved

MarkovChainCLT.tendsto_integral_pow_four_partialSum_div_cube_of_bounded_of_summable_alpha

by IntegralPilot · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

central-limit-theoremmixing-processesprobability

Let $(Y_i)_{i\ge0}$ be a measurable, strictly stationary, centered real sequence on a probability space $(\Omega,P)$ . Suppose there is a real constant $B$ such that $|Y_i|<B$ almost surely for every $i$ , and the strong mixing coefficients satisfy $\sum_{r\ge0}\alpha(r)<\infty$ . Writing $S_n=\sum_{i=0}^{n-1}Y_i$ , one has

\frac{\mathbb E_P[S_n^4]}{n^3}\longrightarrow 0.

This is the fourth-moment estimate used in the independent-block Lindeberg argument for the bounded strongly mixing central limit theorem.

Preamble

import Definitions.Def_MixingCoefficients
import Mathlib

open MeasureTheory ProbabilityTheory Filter MarkovChainCLT
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.tendsto_integral_pow_four_partialSum_div_cube_of_bounded_of_summable_alpha {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : ℕ → Ω → ℝ)
    (hY : ∀ n, Measurable (Y n)) (hstat : IsStrictlyStationary P Y)
    (hcent : ∫ ω, Y 0 ω ∂P = 0)
    (B : ℝ) (hB : ∀ n, ∀ᵐ ω ∂P, |Y n ω| < B)
    (hα : Summable (fun n => alphaMixingCoef P Y n)) :
    Tendsto (fun n : ℕ => (∫ ω, (∑ i ∈ Finset.range n, Y i ω)^4 ∂P) / (n:ℝ)^3)
      atTop (𝓝 0) := by sorry

Source

I. A. Ibragimov and Yu. V. Linnik, Independent and Stationary Sequences of Random Variables (1971), Lemma 18.5.2, p. 348, in the proof of Theorem 18.5.4; https://djvu.online/file/R34Fbtshv2KaJ. The zero-based indexing and almost-sure bound agree with the mission convention.

View graph