Characteristic-function error from a discarded finite selection

Proved

MarkovChainCLT.charFun_sub_le_of_small_selection

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

C=\mathbb E_P[Y_0^2]+2\sum_{k=1}^{\infty}|\mathbb E_P[Y_0Y_k]|.

Let $S$ be a finite selection of indices, $n\ge0$ , and let $F,G$ be measurable real random variables satisfying, pointwise,

F-G=\frac1{\sqrt n}\sum_{i\in S}Y_i.

Writing $\varphi_F(t)=\mathbb E_P e^{itF}$ , for every real $t$ ,

|\varphi_F(t)-\varphi_G(t)|\le |t|\sqrt{\frac{|S|}{n}C}.

This quantifies the effect of deleting a small selection of samples. In particular, if $|S_n|/n\to0$ , the characteristic-function error vanishes. The selected indices may have gaps and need not belong to the first $n$ indices.

Formalization Note Characteristic functions are those of the pushforward laws under $P$ . At $n=0$ , real division and inverse square root use Lean's zero-inverse convention; the hypothesis then says $F=G$ , and the bound is zero.

Preamble

import Definitions.Def_MixingCoefficients
import Mathlib

open MeasureTheory ProbabilityTheory Filter MarkovChainCLT
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.charFun_sub_le_of_small_selection {Ω : 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 : ℕ) (s : Finset ℕ) (F G : Ω → ℝ)
    (hF : Measurable F) (hG : Measurable G)
    (hsub : ∀ ω, F ω - G ω = (Real.sqrt n)⁻¹ * ∑ i ∈ s, Y i ω)
    (t : ℝ) :
    ‖charFun (P.map F) t - charFun (P.map G) t‖ ≤ |t| * Real.sqrt
      (((s.card : ℝ) / n) * ((∫ ω, (Y 0 ω)^2 ∂P) +
        2 * ∑' k : ℕ, |∫ ω, Y 0 ω * Y (k+1) ω ∂P|))  := by sorry

Source

Auxiliary quantitative finite-selection version of the small-block step. Patrick Billingsley, Probability and Measure, 3rd ed., Section 27, pp. 364-367, especially the proof of Theorem 27.4 on p. 367 (discarded blocks and characteristic-function comparison), https://www.colorado.edu/amath/sites/default/files/attached-files/billingsley.pdf. The displayed constant is derived here from the finite-selection variance bound and the elementary exponential Lipschitz inequality; it is not a verbatim theorem from the book.

View graph