Exact moments of a centered real Gaussian

Mathlib records the moment-generating function of gaussianReal, but does not currently expose its moments in all degrees. This file proves the two-step recurrence and the exact even/odd formulas. It is the univariate analytic input for the project's self-contained Isserlis induction.

noncomputable def Anderson4D.centeredGaussianMoment (v : NNReal) (n : ℕ) : ℝ

The n-th raw moment of the centered Gaussian with variance v.

Equations

• Anderson4D.centeredGaussianMoment v n = ∫ (x : ℝ), x ^ n ∂ProbabilityTheory.gaussianReal 0 v

theorem Anderson4D.centeredGaussianMoment_add_two (v : NNReal) (n : ℕ) : centeredGaussianMoment v (n + 2) = (↑n + 1) * ↑v * centeredGaussianMoment v n

Gaussian integration-by-parts recurrence in moment form: E[X^(n+2)] = (n+1) v E[X^n].

def Anderson4D.gaussianPairingCount : ℕ → ℕ

Number of pairings of a 2q-element labeled set, defined by the standard recurrence p(q+1) = (2q+1)p(q).

Equations

• Anderson4D.gaussianPairingCount 0 = 1
• Anderson4D.gaussianPairingCount q.succ = (2 * q + 1) * Anderson4D.gaussianPairingCount q

theorem Anderson4D.centeredGaussianMoment_even (v : NNReal) (q : ℕ) : centeredGaussianMoment v (2 * q) = ↑(gaussianPairingCount q) * ↑v ^ q

Exact even moments of a centered Gaussian.

theorem Anderson4D.centeredGaussianMoment_odd (v : NNReal) (q : ℕ) : centeredGaussianMoment v (2 * q + 1) = 0

Every odd moment of a centered Gaussian vanishes.