← Copula mathematical handbook

The normalizing constant of the Student-t density

We compute the Wallis-type integral

∫_{−π/2}^{π/2} cos^p θ dθ = √π Γ((p+1)/2) / Γ(p/2 + 1), p > −1,

by evaluating E[Z^p ; Z > 0] for a standard normal Z in two ways: directly through the Gamma integral, and in polar coordinates (integral_gaussianReal_prod_of_polar). With the tan substitution of Copula.Families.StudentT.Distribution this gives the classical density

t_n(x) = Γ((n+1)/2) / (√(nπ) Γ(n/2)) · (1 + x²/n)^{−(n+1)/2}.

Main results

• integral_cos_rpow_symm_eq_Gamma: the Wallis integral for real exponents p > −1.
• integral_studentTKernel_eq_Gamma: ∫ (1 + y²/n)^{−(n+1)/2} dy = √(nπ) Γ(n/2)/Γ((n+1)/2).
• studentTPDF_eq: the closed form of the Student-t density.

theorem ProbabilityTheory.integral_Ioi_rpow_gaussianReal {p : ℝ} (hp : -1 < p) : ∫ (x : ℝ), (Set.Ioi 0).indicator (fun (x : ℝ) => x ^ p) x ∂gaussianReal 0 1 = (√(2 * Real.pi))⁻¹ * ((1 / 2) ^ (-(p + 1) / 2) * (1 / 2) * Real.Gamma ((p + 1) / 2))

E[Z^p ; Z > 0] = (2π)^{−1/2} 2^{(p+1)/2} Γ((p+1)/2) / 2 for a standard normal Z.

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

Wallis integral for real exponents: ∫_{−π/2}^{π/2} cos^p θ dθ = √π Γ((p+1)/2) / Γ(p/2 + 1) for p > −1.

theorem ProbabilityTheory.integral_studentTKernel_eq_Gamma {n : ℝ} (hn : 0 < n) : ∫ (y : ℝ), studentTKernel n y = √(n * Real.pi) * Real.Gamma (n / 2) / Real.Gamma ((n + 1) / 2)

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

theorem ProbabilityTheory.studentTPDF_eq {n : ℝ} (hn : 0 < n) (x : ℝ) : studentTPDF n x = Real.Gamma ((n + 1) / 2) / (√(n * Real.pi) * Real.Gamma (n / 2)) * (1 + x ^ 2 / n) ^ (-(n + 1) / 2)

The Student-t density: t_n(x) = Γ((n+1)/2) / (√(nπ) Γ(n/2)) (1 + x²/n)^{−(n+1)/2}.