← Mathematical handbook

theorem Verification.student_precision_density_update {ν t : ℝ} (hν : 0 < ν) (ht : 0 < t) (x : ℝ) : ProbabilityTheory.gammaPDF (ν / 2) (ν / 2) t * ProbabilityTheory.gaussianPDF 0 (NNReal.mk ((√t)⁻¹ ^ 2) ⋯) x = ENNReal.ofReal (studentMarginalPDF ν x) * ProbabilityTheory.gammaPDF (ν / 2 + 1 / 2) (ν / 2 + x ^ 2 / 2) t

theorem Verification.student_precision_measure_update (ν : ℝ) (hν : 0 < ν) (x : ℝ) : ((ProbabilityTheory.gammaMeasure (ν / 2) (ν / 2)).withDensity fun (t : ℝ) => ProbabilityTheory.gaussianPDF 0 (NNReal.mk ((√t)⁻¹ ^ 2) ⋯) x) = ENNReal.ofReal (studentMarginalPDF ν x) • ProbabilityTheory.gammaMeasure (ν / 2 + 1 / 2) (ν / 2 + x ^ 2 / 2)

theorem Verification.student_joint_density_factorization {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (p : ℝ × ℝ) : ENNReal.ofReal (studentJointPDF r ν p) = ENNReal.ofReal (studentMarginalPDF ν p.1) * ∫⁻ (t : ℝ), ProbabilityTheory.gaussianPDF (r * p.1) (NNReal.mk (((√t)⁻¹ * √(1 - r ^ 2)) ^ 2) ⋯) p.2 ∂ProbabilityTheory.gammaMeasure (ν / 2 + 1 / 2) (ν / 2 + p.1 ^ 2 / 2)

noncomputable def Verification.studentConditionalDensity (r ν x y : ℝ) : ENNReal

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.studentConditionalDensity_integral {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (x : ℝ) : ∫⁻ (y : ℝ), studentConditionalDensity r ν x y = 1