Centred Gaussians depend weakly continuously on their variance
ProvedProbabilityTheory.tendsto_integral_gaussianReal_of_tendstoThe centred Gaussian law depends continuously on its variance, in the weak topology. If in then . Concretely: for every bounded Lipschitz ,
Bounded Lipschitz test functions suffice to determine weak convergence (the bounded-Lipschitz metric metrizes it on a separable metric space), so the displayed statement is equivalent to ; it is stated in integral form because that is the form in which it is consumed. Note that no continuity at needs to be excluded: is the Dirac mass at and the statement remains true there.
Where this is used. In the central limit theorem for a square-integrable observable of a uniformly ergodic Markov chain, the observable is truncated at level ; the bounded case gives , and the truncated variances are shown to be Cauchy, say . The final argument then needs to replace by at a cost that vanishes with , which is exactly this lemma.
Proof. Every centred Gaussian is a rescaled standard Gaussian: is the pushforward of under . Changing variables,
the integrand being continuous and bounded, hence integrable. For two variances and the Lipschitz property gives the pointwise bound , so
and the standard Gaussian has a finite first absolute moment. Since is continuous, the right-hand side tends to as , and a squeeze finishes the proof.
import Mathlib.Probability.Distributions.Gaussian.Real import Mathlib.MeasureTheory.Integral.Bochner.Set import Mathlib.MeasureTheory.Measure.Portmanteau open Filter MeasureTheory ProbabilityTheory open scoped ENNReal NNReal Topology
theorem ProbabilityTheory.tendsto_integral_gaussianReal_of_tendsto (u : ℕ → ℝ≥0) (c : ℝ≥0)
(hu : Tendsto (fun K => (u K : ℝ)) atTop (𝓝 (c : ℝ)))
(f : ℝ → ℝ) (L : ℝ≥0) (hL : LipschitzWith L f) (C : ℝ)
(hC : ∀ x y, dist (f x) (f y) ≤ C) :
Tendsto (fun K => ∫ x, f x ∂(gaussianReal 0 (u K))) atTop
(𝓝 (∫ x, f x ∂(gaussianReal 0 c))) := by sorry