← Copula mathematical handbook

The Student-t distribution

For n > 0 degrees of freedom, the Student-t density is t_n(x) = c_n (1 + x²/n)^{-(n+1)/2} with the normalizing constant c_n = (∫ (1 + y²/n)^{-(n+1)/2} dy)⁻¹; we write studentTKernel, studentTPDF and studentTCDF for the unnormalized kernel, the density and the distribution function.

The substitution x = √n tan θ maps (−π/2, π/2) onto ℝ and turns the kernel into √n cos^{n−1} θ dθ, so

T_n(x) = ∫_{−π/2}^{arctan(x/√n)} cos^{n−1} θ dθ / ∫_{−π/2}^{π/2} cos^{n−1} θ dθ

(studentTCDF_eq_angular). In particular, for 0 ≤ a < π/2, T_n(−√n tan a) = ∫_a^{π/2} cos^{n−1} / (2 ∫_0^{π/2} cos^{n−1}) (studentTCDF_neg_sqrt_mul_tan), the identity behind the closed form of the tail-dependence coefficient of the t copula.

Main results

• intervalIntegrable_cos_rpow: cos^p is integrable on [−π/2, π/2] for p > −1.
• integral_Iio_studentTKernel, integral_studentTKernel: the tan substitution.
• integral_studentTPDF: the density integrates to 1.
• studentTCDF_eq_angular, studentTCDF_neg_sqrt_mul_tan.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, Vol. 2, 2nd ed., Wiley 1995, Ch. 28.

noncomputable def ProbabilityTheory.studentTKernel (n x : ℝ) : ℝ

The unnormalized Student-t kernel (1 + x²/n)^{-(n+1)/2}.

Equations

• ProbabilityTheory.studentTKernel n x = (1 + x ^ 2 / n) ^ (-(n + 1) / 2)

noncomputable def ProbabilityTheory.studentTPDF (n x : ℝ) : ℝ

The Student-t density with n degrees of freedom.

Equations

• ProbabilityTheory.studentTPDF n x = ProbabilityTheory.studentTKernel n x / ∫ (y : ℝ), ProbabilityTheory.studentTKernel n y

noncomputable def ProbabilityTheory.studentTCDF (n x : ℝ) : ℝ

The Student-t distribution function with n degrees of freedom.

Equations

• ProbabilityTheory.studentTCDF n x = ∫ (y : ℝ) in Set.Iic x, ProbabilityTheory.studentTPDF n y

theorem ProbabilityTheory.studentTKernel_pos {n : ℝ} (hn : 0 < n) (x : ℝ) : 0 < studentTKernel n x

Integrability of cos^p

theorem ProbabilityTheory.intervalIntegrable_cos_rpow {p : ℝ} (hp : -1 < p) : IntervalIntegrable (fun (θ : ℝ) => Real.cos θ ^ p) MeasureTheory.volume (-(Real.pi / 2)) (Real.pi / 2)

cos^p is integrable on [−π/2, π/2] for p > −1.

theorem ProbabilityTheory.integral_cos_rpow_symm_pos {p : ℝ} (hp : -1 < p) : 0 < ∫ (θ : ℝ) in -(Real.pi / 2)..Real.pi / 2, Real.cos θ ^ p

∫_{−π/2}^{π/2} cos^p > 0 for p > −1.

The tan substitution

theorem ProbabilityTheory.integral_Iio_studentTKernel {n : ℝ} (hn : 0 < n) (x : ℝ) : ∫ (y : ℝ) in Set.Iio x, studentTKernel n y = √n * ∫ (θ : ℝ) in -(Real.pi / 2)..Real.arctan (x / √n), Real.cos θ ^ (n - 1)

The tan substitution: ∫_{−∞}^{x} (1 + y²/n)^{-(n+1)/2} dy = √n ∫_{−π/2}^{arctan(x/√n)} cos^{n−1} θ dθ.

theorem ProbabilityTheory.integral_studentTKernel {n : ℝ} (hn : 0 < n) : ∫ (y : ℝ), studentTKernel n y = √n * ∫ (θ : ℝ) in -(Real.pi / 2)..Real.pi / 2, Real.cos θ ^ (n - 1)

The total mass of the kernel: ∫ (1 + y²/n)^{-(n+1)/2} dy = √n ∫_{−π/2}^{π/2} cos^{n−1}.

theorem ProbabilityTheory.integral_studentTKernel_pos {n : ℝ} (hn : 0 < n) : 0 < ∫ (y : ℝ), studentTKernel n y

theorem ProbabilityTheory.studentTPDF_pos {n : ℝ} (hn : 0 < n) (x : ℝ) : 0 < studentTPDF n x

theorem ProbabilityTheory.integral_studentTPDF {n : ℝ} (hn : 0 < n) : ∫ (x : ℝ), studentTPDF n x = 1

The Student-t density integrates to 1.

theorem ProbabilityTheory.studentTCDF_eq_angular {n : ℝ} (hn : 0 < n) (x : ℝ) : studentTCDF n x = (∫ (θ : ℝ) in -(Real.pi / 2)..Real.arctan (x / √n), Real.cos θ ^ (n - 1)) / ∫ (θ : ℝ) in -(Real.pi / 2)..Real.pi / 2, Real.cos θ ^ (n - 1)

Angular form of the Student-t distribution function.

theorem ProbabilityTheory.integral_cos_rpow_symm {p : ℝ} (hp : -1 < p) : ∫ (θ : ℝ) in -(Real.pi / 2)..Real.pi / 2, Real.cos θ ^ p = 2 * ∫ (θ : ℝ) in 0..Real.pi / 2, Real.cos θ ^ p

∫_{−π/2}^{π/2} cos^p = 2 ∫_0^{π/2} cos^p for p > −1.

theorem ProbabilityTheory.integral_cos_rpow_neg (p a : ℝ) : ∫ (θ : ℝ) in -(Real.pi / 2)..-a, Real.cos θ ^ p = ∫ (θ : ℝ) in a..Real.pi / 2, Real.cos θ ^ p

∫_{−π/2}^{−a} cos^p = ∫_a^{π/2} cos^p.

theorem ProbabilityTheory.studentTCDF_neg_sqrt_mul_tan {n a : ℝ} (hn : 0 < n) (ha : a ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) : studentTCDF n (-(√n * Real.tan a)) = (∫ (θ : ℝ) in a..Real.pi / 2, Real.cos θ ^ (n - 1)) / (2 * ∫ (θ : ℝ) in 0..Real.pi / 2, Real.cos θ ^ (n - 1))

T_n(−√n tan a) = ∫_a^{π/2} cos^{n−1} / (2 ∫_0^{π/2} cos^{n−1}) for a ∈ (−π/2, π/2).