Prove2Me

Bounded sequence with summable α\alpha has absolutely summable autocovariances

Proved
MarkovChainCLT.summable_covariance_of_bounded_of_summable_alpha

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), uniformly bounded in the sense that for some constant BB, ∣Yn∣<B|Y_n|<B almost surely for every nn. Write α(n)\alpha(n) for the strong mixing coefficient of the sequence at lag nn. If

∑n≥0α(n)<∞,\sum_{n\ge 0}\alpha(n)<\infty,

then the positive-lag autocovariance series is absolutely convergent:

∑k≥1∣E[Y0Yk]∣<∞.\sum_{k\ge 1}\left|E[Y_0Y_k]\right|<\infty.

This isolates the covariance-control component of the bounded case of the Ibragimov–Linnik central limit theorem (Jones, Theorem 5, condition 1): it is what makes the asymptotic-variance series σ2=E[Y02]+2∑k≥1E[Y0Yk]\sigma^2=E[Y_0^2]+2\sum_{k\ge 1}E[Y_0Y_k] well defined. The classical route is the covariance inequality for bounded strongly mixing pairs, whose lag-kk bound is a constant multiple of α(k)B2\alpha(k)B^2.

Formalization Note Positive lags are indexed as k+1k+1 for k∈Nk\in\mathbb N, and real summability is unconditional, hence equivalent to absolute convergence. The bound is stated almost surely for each time index separately.

Preamble
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory
Formal statement
/-- The covariance-control component of the Ibragimov–Linnik bounded-case CLT. -/
theorem MarkovChainCLT.summable_covariance_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)) :
    Summable (fun k : ℕ => ∫ ω, Y 0 ω * Y (k + 1) ω ∂P) := 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 5, condition 1 (arXiv v2 p. 9); originals: I. A. Ibragimov, Theory Probab. Appl. 7 (1962); I. A. Ibragimov and Yu. V. Linnik, Independent and Stationary Sequences of Random Variables (1971), Ch. 18

View graph