Prove2Me

Summable ρ\rho implies absolute autocovariance summability

Proved
MarkovChainCLT.summable_covariance_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, and suppose Y0∈L2Y_0\in L^2. If its maximal-correlation mixing coefficients satisfy

∑n≥0ρ(n)<∞,\sum_{n\ge 0}\rho(n)<\infty,

then the positive-lag autocovariance series is absolutely convergent:

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

This isolates the covariance-control component of the summable-ρ\rho central limit theorem and makes the asymptotic-variance series well defined.

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.

Preamble
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory

/-- The covariance-control component of the summable-rho CLT. -/
Formal statement
theorem MarkovChainCLT.summable_covariance_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)) :
    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 7 and eq. (12), arXiv v2 p. 12; original result: I. A. Ibragimov, Theory of Probability and Its Applications 20 (1975).

View graph