The moment generating function of a squared standard Gaussian

This file proves the flagship analytic lemma of the development: if Z ~ N(0,1) then for t < 1/2, E[exp (t · Z²)] = (1 - 2t)^(-1/2).

We phrase the right-hand side as (√(1 - 2t))⁻¹, which is (1-2t)^(-1/2), and which raises cleanly to the k-th power for the chi-squared MGF.

The proof reduces the moment generating function to a Gaussian integral via integral_gaussianReal_eq_integral_smul and then evaluates it with mathlib's integral_gaussian.

noncomputable def JL.stdGaussian : MeasureTheory.Measure ℝ

The standard Gaussian measure N(0,1) on ℝ.

Equations

• JL.stdGaussian = ProbabilityTheory.gaussianReal 0 1

instance JL.instIsProbabilityMeasureRealStdGaussian : MeasureTheory.IsProbabilityMeasure stdGaussian

theorem JL.stdGaussian_pdf (x : ℝ) : ProbabilityTheory.gaussianPDFReal 0 1 x = (√(2 * Real.pi))⁻¹ * Real.exp (-x ^ 2 / 2)

The density of the standard Gaussian, written out.

theorem JL.sqGaussian_mgf {t : ℝ} (ht : t < 1 / 2) : ProbabilityTheory.mgf (fun (x : ℝ) => x ^ 2) stdGaussian t = (√(1 - 2 * t))⁻¹

Squared-Gaussian MGF. For t < 1/2, the moment generating function of Z² with Z ~ N(0,1) is (1 - 2t)^(-1/2) = (√(1 - 2t))⁻¹.