Moments of the real Gaussian distribution

This file computes the centered moments of Mathlib's real Gaussian measure. The absolute centered moment is evaluated first from the Gaussian density and Euler's Gamma integral; the ordinary even and odd centered moments then follow from this formula and symmetry.

The formulas follow the real-Gaussian entry in the StandardDistributions roadmap and the standard calculation in, for example, Johnson, Kotz, and Balakrishnan, Continuous Univariate Distributions, volume 1, Chapter 13.

Main results

• integral_abs_sub_pow_gaussianReal evaluates every absolute centered moment.
• centralMoment_id_two_mul_gaussianReal evaluates the even centered moments.
• centralMoment_id_two_mul_add_one_gaussianReal says that every odd centered moment vanishes.
• integral_sq_gaussianReal evaluates the second raw moment.
• integrable_abs_gaussianReal and integrable_abs_add_abs_gaussianReal give absolute first-moment integrability for one or two Gaussian coordinates.

theorem TauCeti.Probability.integrable_abs_gaussianReal (μ : ℝ) (v : NNReal) : MeasureTheory.Integrable (fun (x : ℝ) => |x|) (ProbabilityTheory.gaussianReal μ v)

The absolute value is integrable under every real Gaussian law.

theorem TauCeti.Probability.integrable_abs_add_abs_gaussianReal (μ₁ μ₂ : ℝ) (v₁ v₂ : NNReal) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => |p.1| + |p.2|) ((ProbabilityTheory.gaussianReal μ₁ v₁).prod (ProbabilityTheory.gaussianReal μ₂ v₂))

The sum of the absolute coordinate values is integrable under two real Gaussian laws.

@[simp]

theorem TauCeti.Probability.integral_abs_sub_pow_gaussianReal (m : ℝ) (v : NNReal) (n : ℕ) : ∫ (x : ℝ), |x - m| ^ n ∂ProbabilityTheory.gaussianReal m v = (2 * ↑v) ^ (↑n / 2) * Real.Gamma ((↑n + 1) / 2) / √Real.pi

The nth absolute centered moment of a real Gaussian distribution.

theorem TauCeti.Probability.integral_abs_gaussianReal (v : NNReal) : ∫ (x : ℝ), |x| ∂ProbabilityTheory.gaussianReal 0 v = √(2 * ↑v / Real.pi)

The mean of the absolute value of a centered real Gaussian, the half-normal mean: E|X| = √(2 * v / π) for X ∼ N(0, v).

@[simp]

theorem TauCeti.Probability.integral_sub_pow_two_mul_gaussianReal (m : ℝ) (v : NNReal) (n : ℕ) : ∫ (x : ℝ), (x - m) ^ (2 * n) ∂ProbabilityTheory.gaussianReal m v = ↑v ^ n * ↑(2 * n - 1).doubleFactorial

The integral of the 2nth power about the mean of a real Gaussian distribution is vⁿ (2n - 1)‼.

@[simp]

theorem TauCeti.Probability.centralMoment_id_two_mul_gaussianReal (m : ℝ) (v : NNReal) (n : ℕ) : ProbabilityTheory.centralMoment id (2 * n) (ProbabilityTheory.gaussianReal m v) = ↑v ^ n * ↑(2 * n - 1).doubleFactorial

The 2nth centered moment of a real Gaussian distribution is vⁿ (2n - 1)‼.

theorem TauCeti.Probability.integral_sq_gaussianReal (m : ℝ) (v : NNReal) : ∫ (x : ℝ), x ^ 2 ∂ProbabilityTheory.gaussianReal m v = ↑v + m ^ 2

The second moment of a real Gaussian distribution is its variance plus its squared mean.

theorem TauCeti.Probability.integral_sub_pow_four_gaussianReal (m : ℝ) (v : NNReal) : ∫ (x : ℝ), (x - m) ^ 4 ∂ProbabilityTheory.gaussianReal m v = 3 * ↑v ^ 2

The fourth centered moment of a real Gaussian distribution is three times its squared variance.

@[simp]

theorem TauCeti.Probability.centralMoment_id_two_mul_add_one_gaussianReal (m : ℝ) (v : NNReal) (n : ℕ) : ProbabilityTheory.centralMoment id (2 * n + 1) (ProbabilityTheory.gaussianReal m v) = 0

Every odd centered moment of a real Gaussian distribution vanishes.