Prove2Me

Change of normalization from σn\sigma_n to n\sqrt n in a Gaussian limit

Proved
MarkovChainCLT.tendstoInDistribution_inv_sqrt_of_normalized

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

central-limit-theoremprobabilityweak-convergence

Let (Xn)n≥1(X_n)_{n\ge1} be real random variables on a probability space and (dn)(d_n) positive normalizing constants such that the self-normalized sequence converges in distribution to a standard Gaussian,

Xndn →d N(0,1),\frac{X_n}{d_n}\ \xrightarrow{d}\ N(0,1),

and such that dn/n→sd_n/\sqrt n\to s with s>0s>0. Then the same sequence normalized by n\sqrt n converges to the Gaussian law of variance s2s^2:

Xnn →d N(0,s2).\frac{X_n}{\sqrt n}\ \xrightarrow{d}\ N(0,s^2).

This is the change-of-normalization step in central limit theorems for dependent sequences: results such as the characterization of the CLT by uniform integrability are stated for Xn/Var(Xn)X_n/\sqrt{\mathrm{Var}(X_n)}, whereas the conclusion sought is for Xn/nX_n/\sqrt n. Since the ratio of the two normalizations is a deterministic sequence converging to ss, the statement is an instance of Slutsky's theorem together with the scaling identity s⋅N(0,1)=N(0,s2)s\cdot N(0,1)=N(0,s^2).

Formalization Note Convergence in distribution is weak convergence of the laws, the limit being the identity random variable on R\mathbb R under the Gaussian measure; the variance of the limit is written as the nonnegative-real coercion of s2s^2.

Preamble
import Definitions.Def_MixingCoefficients
import Mathlib.MeasureTheory.Function.ConvergenceInDistribution
import Mathlib.Probability.Distributions.Gaussian.Real

open MeasureTheory ProbabilityTheory Filter MarkovChainCLT
open scoped ENNReal NNReal Topology ProbabilityTheory
Formal statement
theorem MarkovChainCLT.tendstoInDistribution_inv_sqrt_of_normalized
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (X : ℕ → Ω → ℝ) (d : ℕ → ℝ) (s : ℝ) (hs : 0 < s)
    (hX : ∀ n, Measurable (X n))
    (hd : Tendsto (fun n : ℕ => d n / Real.sqrt n) atTop (𝓝 s))
    (hnorm : TendstoInDistribution (fun (n : ℕ) ω => X n ω / d n) atTop (id : ℝ → ℝ) (fun _ => P)
      (gaussianReal 0 1)) :
    TendstoInDistribution (fun (n : ℕ) ω => (Real.sqrt n)⁻¹ * X n ω) atTop (id : ℝ → ℝ) (fun _ => P)
      (gaussianReal 0 (Real.toNNReal (s ^ 2))) := by sorry
Source
Slutsky's theorem together with the scaling property of the Gaussian law; used in this form in G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Theorems 3 and 5-8, where the CLT is stated once with the normalization sqrt(Var S_n) and once with sqrt(n). See P. Billingsley, Convergence of Probability Measures, 2nd ed. (1999), Theorem 3.1.

View graph