Variance bound for arbitrary finite selections of a stationary sequence

Proved

MarkovChainCLT.variance_finsetSum_le_card_mul_of_summable_abs_cov

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

markov-chainsmcmcprobability

Let $(Y_n)_{n\geq 0}$ be a measurable, strictly stationary sequence of real random variables on a probability space with measure $P$ . Assume that $Y_0$ has mean zero and a finite second moment, and that its positive-lag autocovariances are absolutely summable. Write

\gamma(k)=\mathbb E_P[Y_0Y_k],\qquad \sum_{k=1}^{\infty}|\gamma(k)|<\infty.

For every finite set $S\subseteq\mathbb N$ , the variance of the selected sum satisfies

\operatorname{Var}_P\!\left(\sum_{i\in S}Y_i\right) \leq |S|\left(\mathbb E_P[Y_0^2]+2\sum_{k=1}^{\infty}|\gamma(k)|\right).

The indices in $S$ need not be consecutive. Thus the same constant controls sums over gaps or omitted blocks, which is useful in blocking arguments for central limit theorems. The estimate also includes the empty set and the case of zero variance.

Preamble

import Definitions.Def_MixingCoefficients
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.FunProp

open MeasureTheory ProbabilityTheory Filter MarkovChainCLT
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.variance_finsetSum_le_card_mul_of_summable_abs_cov
    {Ω : 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)
    (hsum : Summable (fun k : ℕ => |∫ ω, Y 0 ω * Y (k + 1) ω ∂P|))
    (s : Finset ℕ) :
    Var[∑ i ∈ s, Y i; P] ≤ (s.card : ℝ) *
      ((∫ ω, (Y 0 ω) ^ 2 ∂P) +
        2 * ∑' k : ℕ, |∫ ω, Y 0 ω * Y (k + 1) ω ∂P|) := by sorry

Source

Auxiliary finite-selection covariance estimate, proved by the row-sum argument in this submission. Reference for the stationary covariance expansion: Patrick Billingsley, Probability and Measure, 3rd edition, Section 27, p. 366, first paragraph of the proof of Theorem 27.4, https://www.colorado.edu/amath/sites/default/files/attached-files/billingsley.pdf. This lemma explicitly extends that covariance calculation to arbitrary finite selections; it is not a verbatim statement of Theorem 27.4. Mission context: Galin L. Jones, On the Markov Chain Central Limit Theorem, Section 4, Theorem 5(ii), https://arxiv.org/html/math/0409112v2.

View graph