← Mathematical handbook

Density and derivative of the Student-t CDF

theorem Verification.studentMarginalPDF_continuous (k : ℝ) (hk : 0 < k) : Continuous (studentMarginalPDF k)

theorem Verification.studentMixture_withDensity (k : ℝ) (hk : 0 < k) : (normalScaleMixtureMarginal (ProbabilityTheory.gammaProbability (k / 2) (k / 2) ⋯ ⋯) fun (t : ℝ) => (√t)⁻¹) = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (studentMarginalPDF k x)

theorem Verification.studentMarginalPDF_integrable (k : ℝ) (hk : 0 < k) : MeasureTheory.Integrable (studentMarginalPDF k) MeasureTheory.volume

theorem Verification.studentMarginalPDF_lintegral (k : ℝ) (hk : 0 < k) : ∫⁻ (x : ℝ), ENNReal.ofReal (studentMarginalPDF k x) = 1

theorem Verification.studentMarginalPDF_integral (k : ℝ) (hk : 0 < k) : ∫ (x : ℝ), studentMarginalPDF k x = 1

theorem Verification.studentTCDF_eq_integral_Iic (k : ℝ) (hk : 0 < k) (x : ℝ) : studentTCDF k x = ∫ (t : ℝ) in Set.Iic x, studentMarginalPDF k t

theorem Verification.studentTCDF_hasDerivAt (k : ℝ) (hk : 0 < k) (z : ℝ) : HasDerivAt (studentTCDF k) (studentMarginalPDF k z) z

theorem Verification.studentTCDF_continuous (k : ℝ) (hk : 0 < k) : Continuous (studentTCDF k)