← Mathematical handbook

theorem Verification.gaussian_rpow_integral (ν b : ℝ) (hν : -1 < ν) (hb : 0 < b) : ∫ (z : ℝ) in Set.Ioi 0, z ^ ν * Real.exp (-(b * z ^ 2)) = (1 / b) ^ ((ν + 1) / 2) * Real.Gamma ((ν + 1) / 2) / 2

theorem Verification.gaussianPositiveMoment_formula (ν : ℝ) (hν : 0 < ν) : gaussianPositiveMoment ν = (√(2 * Real.pi))⁻¹ * (2 ^ ((ν + 1) / 2) * Real.Gamma ((ν + 1) / 2) / 2)

theorem Verification.gaussianPositiveMoment_add_two (ν : ℝ) (hν : 0 < ν) : gaussianPositiveMoment (ν + 2) = (ν + 1) * gaussianPositiveMoment ν