← Mathematical handbook

theorem Verification.studentConditionalDensity_cdf {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (x y : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.volume.withDensity (studentConditionalDensity r ν x))) y = ∫ (t : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((y - r * x) * √t / √(1 - r ^ 2)) ∂ProbabilityTheory.gammaMeasure (ν / 2 + 1 / 2) (ν / 2 + x ^ 2 / 2)

theorem Verification.studentConditionalDensity_cdf_standard {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) (ν : ℝ) (hν : 0 < ν) (x y : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.volume.withDensity (studentConditionalDensity r ν x))) y = ↑(ProbabilityTheory.cdf (normalScaleMixtureMarginal (ProbabilityTheory.gammaProbability ((ν + 1) / 2) ((ν + 1) / 2) ⋯ ⋯) fun (t : ℝ) => (√t)⁻¹)) ((y - r * x) / √((ν + x ^ 2) * (1 - r ^ 2) / (ν + 1)))