← Mathematical handbook

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

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