Independent equal-block Gaussian limit in the bounded mixing case

Proved

MarkovChainCLT.exists_independent_blocks_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, centered, strictly stationary real sequence on a probability space with measure $P$ . Suppose $|Y_i|<B$ almost surely for every $i$ and $\sum_{r\ge0}\alpha(r)<\infty$ . Write

S_r=\sum_{i=0}^{r-1}Y_i,\qquad \sigma^2=\mathbb E_P[Y_0^2]+2\sum_{k=1}^{\infty}\mathbb E_P[Y_0Y_k].

Assume $\operatorname{Var}_P(S_n)/n\to\sigma^2>0$ . There exist integer block lengths $p_n\ge1$ and gap lengths $q_n\ge0$ such that, setting $m_n=\lfloor n/(p_n+q_n)\rfloor$ ,

p_n\to\infty,\quad q_n\to\infty,\quad \frac{p_n}{n}\to0,\quad \frac{n-m_np_n}{n}\to0,\quad (m_n-1)_+\alpha(q_n+1)\to0,

and, for every real $t$ ,

\left(\mathbb E_P e^{itS_{p_n}/\sqrt n}\right)^{m_n}\longrightarrow e^{-\sigma^2t^2/2}.

The final limit concerns a triangular array of independent copies of the big-block sums. Together with the Bernstein comparison estimate, these conclusions give the bounded strongly mixing CLT. The statement isolates the remaining block-schedule and independent-array limit argument; it does not assume independence of the original sequence.

Formalization Note Independent copies are represented through the power of their common characteristic function, so no auxiliary product probability space is needed. The displayed limits concern $n\to\infty$ ; at $n=0$ the inverse convention and zero exponent are harmless.

Preamble

import Definitions.Def_MixingCoefficients
import Mathlib

open MeasureTheory ProbabilityTheory Filter MarkovChainCLT
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.exists_independent_blocks_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))
    (hvarlim : Tendsto (fun n : ℕ => Var[∑ i ∈ Finset.range n, Y i; P] / (n : ℝ))
      atTop (𝓝 (seqAsymptoticVariance P Y)))
    (hvar : 0 < seqAsymptoticVariance P Y) :
    ∃ p q : ℕ → ℕ,
      (∀ n, 0 < p n) ∧
      Tendsto p atTop atTop ∧ Tendsto q atTop atTop ∧
      Tendsto (fun n : ℕ => (p n : ℝ) / n) atTop (𝓝 0) ∧
      Tendsto (fun n : ℕ => ((n - (n / (p n + q n)) * p n : ℕ) : ℝ) / n)
        atTop (𝓝 0) ∧
      Tendsto (fun n : ℕ => ((n / (p n + q n) - 1 : ℕ) : ℝ) *
        alphaMixingCoef P Y (q n + 1)) atTop (𝓝 0) ∧
      ∀ t : ℝ, Tendsto (fun n : ℕ =>
        (charFun (P.map (fun ω => (Real.sqrt n)⁻¹ * ∑ i ∈ Finset.range (p n), Y i ω)) t) ^
          (n / (p n + q n)))
        atTop (𝓝 (charFun (gaussianReal 0 (seqAsymptoticVariance P Y).toNNReal) t)) := by sorry

Source

I. A. Ibragimov and Yu. V. Linnik, Independent and Stationary Sequences of Random Variables (1971), Theorem 18.5.4, pp. 347-350, especially the block construction and independent-array Lindeberg step on pp. 349-350, equations (18.5.18)-(18.5.23); https://djvu.online/file/R34Fbtshv2KaJ. This auxiliary formulation records the schedule and independent-block conclusion together, with the variance limit supplied separately. Mission context: G. L. Jones, On the Markov Chain Central Limit Theorem, Theorem 5(i), https://arxiv.org/html/math/0409112v2.

View graph