← Mathematical handbook

Student-t CDF as a gamma mixture and the chi-type substitution

studentTCDF k x is the CDF at x of the standard Student-t law with k>0 degrees of freedom, written as the normal scale mixture with gamma precision of shape and rate k/2. The main result identifies the positive Gaussian power moment weighted by a normal CDF with a Student-t CDF with ν+1 degrees of freedom. This is the analytic step behind the t-EV Pickands function.

noncomputable def Verification.studentTCDF (k x : ℝ) : ℝ

Standard Student-t CDF with k degrees of freedom, as a gamma-precision normal mixture.

Equations

• Verification.studentTCDF k x = ∫ (t : ℝ), ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (x * √t) ∂ProbabilityTheory.gammaMeasure (k / 2) (k / 2)

theorem Verification.studentTCDF_eq_mixture_cdf (k : ℝ) (hk : 0 < k) (x : ℝ) : studentTCDF k x = ↑(ProbabilityTheory.cdf (normalScaleMixtureMarginal (ProbabilityTheory.gammaProbability (k / 2) (k / 2) ⋯ ⋯) fun (t : ℝ) => (√t)⁻¹)) x

theorem Verification.studentTCDF_strictMono (k : ℝ) (hk : 0 < k) : StrictMono (studentTCDF k)

theorem Verification.studentTCDF_zero (k : ℝ) (hk : 0 < k) : studentTCDF k 0 = 1 / 2

theorem Verification.studentTCDF_neg (k : ℝ) (hk : 0 < k) (x : ℝ) : studentTCDF k (-x) = 1 - studentTCDF k x

theorem Verification.studentTCDF_nonneg (k x : ℝ) : 0 ≤ studentTCDF k x

theorem Verification.studentTCDF_le_one (k : ℝ) (hk : 0 < k) (x : ℝ) : studentTCDF k x ≤ 1

theorem Verification.integral_gammaMeasure_Ioi {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (f : ℝ → ℝ) : ∫ (t : ℝ), f t ∂ProbabilityTheory.gammaMeasure a b = ∫ (t : ℝ) in Set.Ioi 0, ProbabilityTheory.gammaPDFReal a b t * f t

Gamma integrals of bounded functions as Lebesgue integrals over the positive half-line.

theorem Verification.integral_Ioi_rpow_gaussian_subst (ν : ℝ) (hν : 0 < ν) (g : ℝ → ℝ) : ∫ (z : ℝ) in Set.Ioi 0, z ^ ν * Real.exp (-(z ^ 2 / 2)) * g z = (ν + 1) ^ ((ν + 1) / 2) / 2 * ∫ (t : ℝ) in Set.Ioi 0, t ^ ((ν - 1) / 2) * Real.exp (-((ν + 1) / 2 * t)) * g √((ν + 1) * t)

The chi-type substitution t=z²/(ν+1) on the positive half-line.

theorem Verification.positivePower_normalCDF_integral (ν : ℝ) (hν : 0 < ν) (β : ℝ) : ∫ (z : ℝ), positivePower ν z * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (β * z) ∂ProbabilityTheory.gaussianReal 0 1 = gaussianPositiveMoment ν * studentTCDF (ν + 1) (β * √(ν + 1))

The positive Gaussian power moment weighted by a normal CDF is a Student-t CDF with ν+1 degrees of freedom.