Bernstein block comparison with an explicit discarded-sample bound

Proved

MarkovChainCLT.charFun_sub_pow_block_le

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$ , with $Y_0\in L^2(P)$ and absolutely summable positive-lag autocovariances. Write

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

Fix a sample size $n\ge0$ , a positive block length $p$ , and a gap length $q\ge0$ . Retain $m=\lfloor n/(p+q)\rfloor$ blocks of length $p$ , beginning at indices $j(p+q)$ for $0\le j<m$ . There are exactly $r=n-mp$ discarded indices, counting the gaps and final remainder. Let $\alpha$ denote the strong-mixing coefficient of the sequence.

For every real $t$ ,

\left|\mathbb E_P e^{itS_n/\sqrt n}-\left(\mathbb E_P e^{itS_p/\sqrt n}\right)^m\right| \le |t|\sqrt{\frac{r}{n}C}+16(m-1)_+\alpha(q+1).

The power on the left is the characteristic function of a sum of $m$ independent variables, each with the distribution of $S_p/\sqrt n$ . The two terms on the right separately control discarded samples and dependence between retained blocks. This finite-sample comparison is reusable in blocking proofs of central limit theorems.

Formalization Note The gap is $q+1$ in the platform's inclusive-endpoint mixing convention. Natural subtraction gives $(m-1)_+=0$ for $m=0$ . Zero inverse is used at $n=0$ , where both characteristic functions on the left equal one.

Preamble

import Definitions.Def_MixingCoefficients
import Mathlib

open MeasureTheory ProbabilityTheory Filter MarkovChainCLT
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.charFun_sub_pow_block_le {Ω : 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|))
    (n p q : ℕ) (hp : 0 < p) (t : ℝ) :
    ‖charFun (P.map (fun ω => (Real.sqrt n)⁻¹ * ∑ i ∈ Finset.range n, Y i ω)) t -
      (charFun (P.map (fun ω => (Real.sqrt n)⁻¹ * ∑ i ∈ Finset.range p, Y i ω)) t) ^
        (n / (p+q))‖ ≤
    |t| * Real.sqrt (((n - (n/(p+q))*p : ℕ) : ℝ) / n *
      ((∫ ω, (Y 0 ω)^2 ∂P) + 2 * ∑' k : ℕ, |∫ ω, Y 0 ω * Y (k+1) ω ∂P|)) +
      16 * ((n/(p+q)-1 : ℕ) : ℝ) * alphaMixingCoef P Y (q+1)  := by sorry

Source

Auxiliary finite-sample Bernstein comparison, with all counting and boundary conventions explicit. Patrick Billingsley, Probability and Measure, 3rd ed., Section 27, equations (27.21)-(27.23), pp. 364-365, and the proof of Theorem 27.4, p. 367, https://www.colorado.edu/amath/sites/default/files/attached-files/billingsley.pdf. I. A. Ibragimov and Yu. V. Linnik, Independent and Stationary Sequences of Random Variables (1971), Sections 18.4-18.5, proof of Theorem 18.5.4, pp. 349-350, https://djvu.online/file/R34Fbtshv2KaJ. This formulation combines that comparison with the arbitrary-selection variance estimate.

View graph