Degenerate case $\sigma^2 = 0$ : $S_n/\sqrt{n} \to \delta_0$

Proved

MarkovChainCLT.stationary_clt_of_asymptoticVariance_nonpos

by wenxinzhang · Aug 18, 2026 · Mathlib c5ea003 (Lean v4.30.0)

central-limit-theoremmarkov-chainsprobability

The degenerate branch of the Markov-chain CLT: zero asymptotic variance.

Let $P$ be a Harris ergodic Markov kernel with invariant probability measure $\pi$ , let $f \in L^2(\pi)$ , write $c = E_\pi f$ and $Y_i(\omega) = f(\omega_i) - c$ for the centered functional along the stationary chain, and suppose the covariance series $\sum_k E[Y_0 Y_{k+1}]$ converges absolutely, so that the asymptotic variance

\sigma^2 \;=\; E[Y_0^2] + 2\sum_{k \ge 1} E[Y_0 Y_k]

is well defined. If $\sigma^2 \le 0$ , then

\frac{1}{\sqrt n}\sum_{i=0}^{n-1} Y_i \;\longrightarrow_d\; N(0, \sigma^2_+) \;=\; \delta_0 .

Jones (2004) states Theorems 5–8 under the standing assumption $\sigma^2 > 0$ , which is the only case of practical interest: it is what makes the limit a genuine Gaussian and the Monte Carlo error bars meaningful. This statement is the complementary branch, and it is exactly what a formalization needs in order to conclude the mission's unconditional SatisfiesCLT predicate, which permits a degenerate limit $v = 0$ (convergence to the point mass at $0$ ).

Mathematically the content is that under stationarity and absolute convergence of the covariance series one has $\mathrm{Var}(S_n)/n \to \sigma^2$ ; when $\sigma^2 = 0$ this forces $S_n/\sqrt n \to 0$ in $L^2$ , hence in probability, hence in distribution to $\delta_0$ . Note $\sigma^2 \ge 0$ always holds under these hypotheses, so " $\sigma^2 \le 0$ " is really the single case $\sigma^2 = 0$ ; it is phrased as an inequality only so that it is the exact logical complement of the hypothesis $0 < \sigma^2$ carried by the mission's other CLT statements, letting the two branches be combined without a side condition.

Formalization Note seqAsymptoticVariance is the mission's $\sigma^2$ ; .toNNReal sends the degenerate value to $0$ , so the limit law gaussianReal 0 0 is the Dirac mass at $0$ . Indexing starts at $0$ , matching the mission's convention.

Preamble

import Definitions.Def_MarkovErgodicity
import Definitions.Def_MarkovChainPathMeasure
import Definitions.Def_MixingCoefficients

open MeasureTheory ProbabilityTheory Filter
open scoped ENNReal NNReal Topology ProbabilityTheory

Formal statement

theorem MarkovChainCLT.stationary_clt_of_asymptoticVariance_nonpos {X : Type*} [MeasurableSpace X]
    (P : Kernel X X) [IsMarkovKernel P] (π : Measure X) [IsProbabilityMeasure π]
    (hP : HarrisErgodic P π) (f : X → ℝ) (hf : Measurable f) (hL2 : MemLp f 2 π)
    (hsum : Summable (fun k : ℕ => ∫ ω, (f (ω 0) - ∫ x, f x ∂π) *
        (f (ω (k + 1)) - ∫ x, f x ∂π) ∂(chainMeasure P π)))
    (hzero : seqAsymptoticVariance (chainMeasure P π)
      (fun i ω => f (ω i) - ∫ x, f x ∂π) ≤ 0) :
    TendstoInDistribution
      (fun (n : ℕ) (ω : ℕ → X) => (Real.sqrt n)⁻¹ *
        ∑ i ∈ Finset.range n, (f (ω i) - ∫ x, f x ∂π))
      atTop (id : ℝ → ℝ) (fun _ => chainMeasure P π)
      (gaussianReal 0 (seqAsymptoticVariance (chainMeasure P π)
        (fun i ω => f (ω i) - ∫ x, f x ∂π)).toNNReal) := by sorry

Source

G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Section 4: the asymptotic variance sigma^2 = E[Y_0^2] + 2 sum_{k>=1} E[Y_0 Y_k] of Theorems 5-8, which Jones states under the standing assumption sigma^2 > 0. This is the complementary degenerate branch sigma^2 = 0, required to obtain the unconditional CLT conclusion (Jones eq. (1)); it is not separately numbered in the paper.

View graph

Degenerate case σ2=0\sigma^2 = 0σ2=0: Sn/n→δ0S_n/\sqrt{n} \to \delta_0Sn​/n​→δ0​

Degenerate case $\sigma^2 = 0$ : $S_n/\sqrt{n} \to \delta_0$