Prove2Me

Characteristic-function convergence for a strongly mixing stationary sequence with a 2+δ2+\delta moment

Proved
MarkovChainCLT.charFun_tendsto_of_alpha_pow_summable

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

markov-chainsmcmcprobability

Characteristic-function convergence for the strongly mixing moment case (the analytic core of the Ibragimov-Linnik CLT).

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) with E∣Y0∣2+δ<∞E|Y_0|^{2+\delta}<\infty for some δ>0\delta>0 and strong mixing coefficients satisfying ∑n≥0α(n)δ/(2+δ)<∞\sum_{n\ge 0}\alpha(n)^{\delta/(2+\delta)}<\infty. Assume also that the positive-lag autocovariance series ∑k≥1E[Y0Yk]\sum_{k\ge 1}E[Y_0Y_k] is absolutely convergent, and set

σ2=E[Y02]+2∑k≥1E[Y0Yk]>0.\sigma^2=E[Y_0^2]+2\sum_{k\ge 1}E[Y_0Y_k]>0 .

Then the characteristic functions of the laws of the normalised partial sums converge pointwise to the characteristic function of N(0,σ2)N(0,\sigma^2): for every t∈Rt\in\mathbb R,

∫exp⁡ ⁣(it (n)−1∑i<nYi) dP  ⟶  e−σ2t2/2(n→∞).\int \exp\!\Bigl(i t\,(\sqrt n)^{-1}\textstyle\sum_{i<n}Y_i\Bigr)\,dP \;\longrightarrow\; e^{-\sigma^2 t^2/2}\qquad (n\to\infty).

Why this is the right split. The classical proofs of Theorem 5(ii) - Ibragimov (1962), and Ibragimov & Linnik (1971, Theorem 18.5.3), which Jones quotes verbatim - run in exactly two steps: first the semi-invariant/blocking estimates show that the characteristic functions of n−1/2Snn^{-1/2}S_n converge to those of the Gaussian; then Levy's continuity theorem upgrades this to weak convergence of the laws. This lemma isolates the first, analytic step, and it is the only content left in tendstoInDistribution_of_alpha_pow_summable: that distributional leaf follows from this statement plus Levy's theorem (MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_charFun, which Mathlib proves via Prokhorov). Stating the estimate on its own separates the hard analysis from the topological conclusion and makes it reusable: every mixing CLT in this mission has the same distributional target, and Mathlib's own iid central limit theorem is proved by the same characteristic-function route.

Formalization Note The law of the normalised sum is written as a pushforward P.map (fun ω => (Real.sqrt n)⁻¹ * ∑ i ∈ Finset.range n, Y i ω), and characteristic functions are Mathlib's MeasureTheory.charFun, so the limit is expressed as convergence of charFun values into C\mathbb C; the Gaussian characteristic function is that of gaussianReal 0 (σ²).toNNReal.

Preamble
import Definitions.Def_MixingCoefficients
import Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
import Mathlib.Probability.Distributions.Gaussian.Real
import Mathlib.Analysis.SpecialFunctions.Pow.Real

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory
Formal statement
theorem MarkovChainCLT.charFun_tendsto_of_alpha_pow_summable
    {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) [IsProbabilityMeasure P] (Y : ℕ → Ω → ℝ)
    (hY : ∀ n, Measurable (Y n)) (hstat : IsStrictlyStationary P Y)
    (hcent : ∫ ω, Y 0 ω ∂P = 0)
    (δ : ℝ) (hδ : 0 < δ) (hmom : Integrable (fun ω => |Y 0 ω| ^ (2 + δ)) P)
    (hα : Summable (fun n => alphaMixingCoef P Y n ^ (δ / (2 + δ))))
    (hsum : Summable (fun k : ℕ => ∫ ω, Y 0 ω * Y (k + 1) ω ∂P))
    (hvar : 0 < seqAsymptoticVariance P Y) :
    ∀ t : ℝ,
      Tendsto (fun n : ℕ =>
          charFun (P.map (fun ω =>
            (Real.sqrt n)⁻¹ * ∑ i ∈ Finset.range n, Y i ω)) t)
        atTop (𝓝 (charFun (gaussianReal 0 (seqAsymptoticVariance P Y).toNNReal) t)) := 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 2, eq. (10) (arXiv v2 p. 9), whose cited proofs are: I. A. Ibragimov, "Some limit theorems for stationary processes", Theory Probab. Appl. 7 (1962) - proved via characteristic functions; and I. A. Ibragimov & Yu. V. Linnik, "Independent and Stationary Sequences of Random Variables" (1971), Theorem 18.5.3 (semi-invariant / characteristic-function method). This lemma isolates the characteristic-function step of that method; the topological step is Levy's continuity theorem.

View graph