← Mathematical handbook

theorem Verification.measurable_studentConditionalDensity {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) : Measurable fun (p : ℝ × ℝ) => studentConditionalDensity r ν p.1 p.2

theorem Verification.student_marginal_density {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) (i : Fin 2) : ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) i = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (studentMarginalPDF ν x)

theorem Verification.student_joint_disintegration {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (f : ℝ × ℝ → ENNReal) (hf : Measurable f) : ∫⁻ (p : ℝ × ℝ), f p ∂MeasureTheory.Measure.map ⇑MeasurableEquiv.finTwoArrow ↑(ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) = ∫⁻ (x : ℝ), ∫⁻ (y : ℝ), f (x, y) ∂MeasureTheory.volume.withDensity (studentConditionalDensity r ν x) ∂ProbabilityTheory.Copula.marginal (ProbabilityTheory.Copula.studentTLaw (bivariateCorrelation r) ν hν) 0