← Copula mathematical handbook

The margins of the multivariate Student-t law

The library constructs the Student-t copula from the scale mixture studentTLaw R ν, the law of G^{-1/2} Z with Z ~ N(0, R) independent of G ~ Gamma(ν/2, ν/2). Here we show that every one-dimensional margin of this law is the classical Student-t distribution with ν degrees of freedom (R i i = 1):

P(G^{-1/2} Z_i ∈ dx) = t_ν(x) dx, t_ν(x) = c_ν (1 + x²/ν)^{-(ν+1)/2}.

Consequently the marginal distribution functions used in the Sklar construction of studentT are the Student-t distribution function studentTCDF ν, and the t copula is the copula of the multivariate t distribution with t_ν margins: C(T_ν(x₁), …, T_ν(x_d)) = P(X₁ ≤ x₁, …, X_d ≤ x_d).

Proof

Conditionally on G = g > 0, G^{-1/2} Z_i ~ N(0, 1/g), with density √g (2π)^{-1/2} e^{-g x²/2}. By Tonelli, the density of the mixture is

∫_0^∞ (ν/2)^{ν/2}/Γ(ν/2) g^{ν/2-1} e^{-νg/2} √g (2π)^{-1/2} e^{-g x²/2} dg = K_ν (1 + x²/ν)^{-(ν+1)/2}

by the Gamma integral; the constant K_ν is identified with 1 / ∫ (1 + y²/ν)^{-(ν+1)/2} dy because both sides are probability densities.

Main results

• studentTMeasure ν: the Student-t distribution, volume.withDensity (studentTPDF ν).
• cdf_studentTMeasure: its distribution function is studentTCDF ν.
• marginal_gaussianScaleMixtureLaw: margins of Gaussian scale mixtures.
• map_gaussianReal_prod_gammaMeasure: the law of G^{-1/2} Z is studentTMeasure ν.
• marginal_studentTLaw, cdf_marginal_studentTLaw.
• cdf_studentT_studentTCDF, eq_studentT_of_cdf: the t copula is the (unique) copula of the t law with t_ν margins; cdf_studentT_corrMatrix is the bivariate form.

References

• S. Kotz, S. Nadarajah, Multivariate t Distributions and Their Applications, CUP 2004, Ch. 1.
• S. Demarta, A. McNeil, The t copula and related copulas, Int. Stat. Rev. 73 (2005).

The Student-t distribution as a measure

noncomputable def ProbabilityTheory.studentTMeasure (ν : ℝ) : MeasureTheory.Measure ℝ

The Student-t distribution with ν degrees of freedom, as a measure on ℝ.

Equations

• ProbabilityTheory.studentTMeasure ν = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (ProbabilityTheory.studentTPDF ν x)

theorem ProbabilityTheory.integrable_studentTKernel {ν : ℝ} (hν : 0 < ν) : MeasureTheory.Integrable (studentTKernel ν) MeasureTheory.volume

theorem ProbabilityTheory.integrable_studentTPDF {ν : ℝ} (hν : 0 < ν) : MeasureTheory.Integrable (studentTPDF ν) MeasureTheory.volume

theorem ProbabilityTheory.isProbabilityMeasure_studentTMeasure {ν : ℝ} (hν : 0 < ν) : MeasureTheory.IsProbabilityMeasure (studentTMeasure ν)

theorem ProbabilityTheory.studentTMeasure_real_apply {ν : ℝ} (hν : 0 < ν) {S : Set ℝ} (hS : MeasurableSet S) : (studentTMeasure ν).real S = ∫ (x : ℝ) in S, studentTPDF ν x

P(T ∈ S) = ∫_S t_ν for the Student-t distribution.

theorem ProbabilityTheory.cdf_studentTMeasure {ν : ℝ} (hν : 0 < ν) : ↑(cdf (studentTMeasure ν)) = studentTCDF ν

The distribution function of studentTMeasure ν is studentTCDF ν.

theorem ProbabilityTheory.studentTCDF_nonneg {ν : ℝ} (hν : 0 < ν) (x : ℝ) : 0 ≤ studentTCDF ν x

theorem ProbabilityTheory.studentTCDF_le_one {ν : ℝ} (hν : 0 < ν) (x : ℝ) : studentTCDF ν x ≤ 1

The gamma mixture of centered normal laws

theorem ProbabilityTheory.map_gaussianReal_prod_gammaMeasure {ν : ℝ} (hν : 0 < ν) : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => (√p.2)⁻¹ * p.1) ((gaussianReal 0 1).prod (gammaMeasure (ν / 2) (ν / 2))) = studentTMeasure ν

The law of G^{-1/2} Z for Z ~ N(0, 1) independent of G ~ Gamma(ν/2, ν/2) is the Student-t distribution with ν degrees of freedom.

theorem ProbabilityTheory.Copula.marginal_gaussianScaleMixtureLaw {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) {s : ℝ → ℝ} (hs : Measurable s) (i : Fin d) : marginal (gaussianScaleMixtureLaw R μ s) i = MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => s p.2 * p.1) ((gaussianReal 0 1).prod ↑μ)

Margins of a Gaussian scale mixture: if R i i = 1, the ith coordinate of s(T) · Z has the law of s(T) · Z₀ with Z₀ ~ N(0, 1) independent of T.

theorem ProbabilityTheory.Copula.marginal_studentTLaw {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) {ν : ℝ} (hν : 0 < ν) (i : Fin d) : marginal (studentTLaw R ν hν) i = studentTMeasure ν

The margins of the multivariate t law are Student-t distributions: every coordinate of studentTLaw R ν (with unit diagonal) has the density studentTPDF ν.

theorem ProbabilityTheory.Copula.cdf_marginal_studentTLaw {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) {ν : ℝ} (hν : 0 < ν) (i : Fin d) : ↑(ProbabilityTheory.cdf (marginal (studentTLaw R ν hν) i)) = studentTCDF ν

The marginal distribution functions of the t law are studentTCDF ν.

theorem ProbabilityTheory.Copula.marginalTransform_studentTLaw {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) {ν : ℝ} (hν : 0 < ν) (x : Fin d → ℝ) : marginalTransform (studentTLaw R ν hν) x = fun (i : Fin d) => cdfUnit (studentTMeasure ν) (x i)

The probability integral transform of the Sklar construction is the Student-t CDF.

theorem ProbabilityTheory.Copula.cdf_studentT_studentTCDF {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) {ν : ℝ} (hν : 0 < ν) (x : Fin d → ℝ) : ((studentT R hR hdiag ν hν).cdf fun (i : Fin d) => cdfUnit (studentTMeasure ν) (x i)) = (↑(studentTLaw R ν hν)).real (Set.Iic x)

The t copula is the copula of the multivariate t distribution with t_ν margins: C(T_ν(x₁), …, T_ν(x_d)) = P(X ≤ x) where T_ν = studentTCDF ν.

theorem ProbabilityTheory.Copula.eq_studentT_of_cdf {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) {ν : ℝ} (hν : 0 < ν) (C : Copula d) (hC : ∀ (x : Fin d → ℝ), (C.cdf fun (i : Fin d) => cdfUnit (studentTMeasure ν) (x i)) = (↑(studentTLaw R ν hν)).real (Set.Iic x)) : C = studentT R hR hdiag ν hν

Uniqueness: a copula C with C(T_ν(x₁), …, T_ν(x_d)) = P(X ≤ x) for all x is the t copula.

theorem ProbabilityTheory.Copula.cdf_studentT_corrMatrix {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) {ν : ℝ} (hν : 0 < ν) (x y : ℝ) : (studentT (corrMatrix r) ⋯ ⋯ ν hν).cdf ![cdfUnit (studentTMeasure ν) x, cdfUnit (studentTMeasure ν) y] = (↑(studentTLaw (corrMatrix r) ν hν)).real {z : Fin 2 → ℝ | z 0 ≤ x ∧ z 1 ≤ y}

Bivariate form: for the bivariate t law (X, Y) with correlation r, C_{ν,r}(T_ν(x), T_ν(y)) = P(X ≤ x, Y ≤ y).

theorem ProbabilityTheory.continuous_studentTCDF {ν : ℝ} (hν : 0 < ν) : Continuous (studentTCDF ν)

The Student-t distribution function is continuous.