← Mathematical handbook

theorem Verification.gaussianPDFReal_inverse_sqrt {t : ℝ} (ht : 0 < t) (x : ℝ) : ProbabilityTheory.gaussianPDFReal 0 (NNReal.mk ((√t)⁻¹ ^ 2) ⋯) x = (√(2 * Real.pi))⁻¹ * t ^ (1 / 2) * Real.exp (-(x ^ 2 / 2 * t))

noncomputable def Verification.studentMarginalPDF (ν x : ℝ) : ℝ

Equations

• Verification.studentMarginalPDF ν x = (√(2 * Real.pi))⁻¹ * ((ν / 2) ^ (ν / 2) / Real.Gamma (ν / 2) * Real.Gamma (ν / 2 + 1 / 2) / (ν / 2 + x ^ 2 / 2) ^ (ν / 2 + 1 / 2))

theorem Verification.studentMarginalPDF_pos {ν : ℝ} (hν : 0 < ν) (x : ℝ) : 0 < studentMarginalPDF ν x

theorem Verification.student_marginal_density_evaluation (ν : ℝ) (hν : 0 < ν) (x : ℝ) : normalScaleMixtureDensity (ProbabilityTheory.gammaProbability (ν / 2) (ν / 2) ⋯ ⋯) (fun (t : ℝ) => (√t)⁻¹) x = ENNReal.ofReal (studentMarginalPDF ν x)

theorem Verification.studentMarginalPDF_standard_form {ν : ℝ} (hν : 0 < ν) (x : ℝ) : studentMarginalPDF ν x = Real.Gamma ((ν + 1) / 2) / (√(ν * Real.pi) * Real.Gamma (ν / 2)) * (1 + x ^ 2 / ν) ^ (-((ν + 1) / 2))