← Copula mathematical handbook

Regularly varying tails of the bivariate Student-t law

Let (X, Y) = G^{-1/2} (Z₁, Z₂) with (Z₁, Z₂) ~ bivariateNormal r independent of G ~ Gamma(ν/2, ν/2) (the library's studentTLaw (corrMatrix r) ν). For y > 0 and a positively homogeneous functional f,

P(f(X, Y) ≥ y) = E[P(G < max(f(Z), 0)² / y²)],

and the small-ball behaviour of the gamma law (Copula.Families.StudentT.GammaSmallBall) together with dominated convergence gives

y^ν P(f(X, Y) ≥ y) → K E[max(f(Z), 0)^ν], K = (ν/2)^{ν/2} / ((ν/2) Γ(ν/2)).

Applied to f = min(−x, −y) and f = −x this yields the regularly varying joint and marginal lower tails of the Student-t law, with limits K · normalJointTailMoment ν r and K · normalTailMoment ν.

References

• P. Embrechts, A. McNeil, D. Straumann, Correlation and dependence in risk management: properties and pitfalls, CUP 2002.
• H. Hult, F. Lindskog, Multivariate extremes, aggregation and dependence in elliptical distributions, Adv. Appl. Probab. 34 (2002).

theorem ProbabilityTheory.Copula.setOf_le_inv_sqrt_mul {y : ℝ} (hy : 0 < y) (m : ℝ) : {t : ℝ | y ≤ (√t)⁻¹ * m} = Set.Ioc 0 (max m 0 ^ 2 / y ^ 2)

For y > 0: {t | y ≤ t^{-1/2} m} = (0, max(m, 0)²/y²].

theorem ProbabilityTheory.Copula.gammaMeasure_real_Ioc_eq {a b : ℝ} (q : ℝ) : (gammaMeasure a b).real (Set.Ioc 0 q) = (gammaMeasure a b).real (Set.Iio q)

P(0 < G ≤ q) = P(G < q) for a gamma variable.

theorem ProbabilityTheory.Copula.monotone_gammaMeasure_real_Iio {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Monotone fun (q : ℝ) => (gammaMeasure a b).real (Set.Iio q)

theorem ProbabilityTheory.Copula.studentTLaw_real_le_eq {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) {ν : ℝ} (hν : 0 < ν) {y : ℝ} (hy : 0 < y) (f : ℝ × ℝ → ℝ) (hf : Measurable f) (hhom : ∀ (c : ℝ), 0 ≤ c → ∀ (p : ℝ × ℝ), f (c * p.1, c * p.2) = c * f p) : (↑(studentTLaw (corrMatrix r) ν hν)).real {z : Fin 2 → ℝ | y ≤ f (z 0, z 1)} = ∫ (p : ℝ × ℝ), (gammaMeasure (ν / 2) (ν / 2)).real (Set.Iio (max (f p) 0 ^ 2 / y ^ 2)) ∂bivariateNormal r

Orthant probabilities of the Student-t law as Gaussian integrals. For y > 0 and a measurable, positively homogeneous f, P(y ≤ f(X, Y)) = E[P(G < max(f(Z₁, Z₂), 0)² / y²)].

theorem ProbabilityTheory.Copula.tendsto_rpow_mul_integral_gammaMeasure_real_Iio {E : Type u_1} [MeasurableSpace E] {P : MeasureTheory.Measure E} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) {f : E → ℝ} (hf : Measurable f) (hint : MeasureTheory.Integrable (fun (p : E) => max (f p) 0 ^ (2 * a)) P) : Filter.Tendsto (fun (y : ℝ) => y ^ (2 * a) * ∫ (p : E), (gammaMeasure a b).real (Set.Iio (max (f p) 0 ^ 2 / y ^ 2)) ∂P) Filter.atTop (nhds (gammaSmallBallConst a b * ∫ (p : E), max (f p) 0 ^ (2 * a) ∂P))

Dominated convergence for the scaled gamma tails. If max(f, 0)^{2a} is integrable, then y^{2a} E[P(G < max(f, 0)²/y²)] → K E[max(f, 0)^{2a}].

noncomputable def ProbabilityTheory.Copula.studentTTailConst (ν : ℝ) : ℝ

The small-ball constant of the Student-t mixing law Gamma(ν/2, ν/2).

Equations

• ProbabilityTheory.Copula.studentTTailConst ν = ProbabilityTheory.gammaSmallBallConst (ν / 2) (ν / 2)

theorem ProbabilityTheory.Copula.studentTTailConst_pos {ν : ℝ} (hν : 0 < ν) : 0 < studentTTailConst ν

theorem ProbabilityTheory.Copula.tendsto_rpow_mul_studentTLaw_lowerOrthant {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) {ν : ℝ} (hν : 0 < ν) : Filter.Tendsto (fun (y : ℝ) => y ^ ν * (↑(studentTLaw (corrMatrix r) ν hν)).real {z : Fin 2 → ℝ | z 0 ≤ -y ∧ z 1 ≤ -y}) Filter.atTop (nhds (studentTTailConst ν * normalJointTailMoment ν r))

The joint lower tail of the Student-t law is regularly varying with index −ν: y^ν P(X ≤ −y, Y ≤ −y) → K E[max(min(Z₁, Z₂), 0)^ν].

theorem ProbabilityTheory.Copula.tendsto_rpow_mul_studentTLaw_lowerTail {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) {ν : ℝ} (hν : 0 < ν) : Filter.Tendsto (fun (y : ℝ) => y ^ ν * (↑(studentTLaw (corrMatrix r) ν hν)).real {z : Fin 2 → ℝ | z 0 ≤ -y}) Filter.atTop (nhds (studentTTailConst ν * normalTailMoment ν))

The marginal lower tail of the Student-t law: y^ν P(X ≤ −y) → K E[max(Z, 0)^ν].