← Copula mathematical handbook

Monotonicity of the Student-t tail-dependence coefficient

The tail-dependence coefficient of the bivariate Student-t copula with ν > 0 degrees of freedom and correlation r ∈ [−1, 1] has the angular form (studentTTailCoeff)

λ(ν, r) = ∫_a^{π/2} cos^ν θ dθ / ∫_0^{π/2} cos^ν θ dθ, a = arccos(r) / 2.

We prove the classical qualitative behaviour of λ (Embrechts–McNeil–Straumann 2002, Demarta–McNeil 2005, Fig. 1):

• λ(ν, ·) is strictly increasing on [−1, 1]: the lower limit arccos(r)/2 decreases.
• λ(·, r) is strictly decreasing on (0, ∞) for r ∈ (−1, 1). Writing N_ν = ∫_a^{π/2} cos^ν, B_ν = ∫_0^a cos^ν and c = cos(a)^{μ−ν} for ν < μ, the factor cos^{μ−ν} is ≤ c on [a, π/2] and ≥ c on [0, a] (strictly at 0), so N_μ ≤ c N_ν and c B_ν < B_μ; hence N_μ B_ν < N_ν B_μ, which is λ(μ, r) < λ(ν, r) (a Chebyshev-type ratio argument).
• λ(ν, r) → 0 as ν → ∞ for every r < 1, consistent with the tail independence of the Gaussian copula (hasLowerTailDependence_bivariateGaussian): indeed λ(ν, r) ≤ ((π − 2a)/a) · (cos a / cos(a/2))^ν.
• λ(ν, r) → 1 − arccos(r)/π as ν → 0⁺ (dominated convergence); this is the supremum of the coefficient over ν (studentTTailCoeff_lt_limit).

Main results

• studentTTailCoeff_strictMonoOn, studentTTailCoeff_monotone: monotonicity in r.
• studentTTailCoeff_strictAntiOn: strict monotonicity in ν.
• tendsto_studentTTailCoeff_atTop: λ(ν, r) → 0 as ν → ∞ (r < 1).
• tendsto_studentTTailCoeff_nhdsGT_zero: λ(ν, r) → 1 − arccos(r)/π as ν → 0⁺.

References

• P. Embrechts, A. McNeil, D. Straumann, Correlation and dependence in risk management: properties and pitfalls, CUP 2002.
• S. Demarta, A. McNeil, The t copula and related copulas, Int. Stat. Rev. 73 (2005).

Monotonicity in the correlation

theorem ProbabilityTheory.Copula.studentTTailCoeff_monotone {ν : ℝ} (hν : 0 < ν) : Monotone (studentTTailCoeff ν)

Monotonicity in r: λ(ν, ·) is monotone on ℝ (it is constant outside [−1, 1]).

theorem ProbabilityTheory.Copula.studentTTailCoeff_strictMonoOn {ν : ℝ} (hν : 0 < ν) : StrictMonoOn (studentTTailCoeff ν) (Set.Icc (-1) 1)

Strict monotonicity in r: λ(ν, ·) is strictly increasing on [−1, 1] (Embrechts–McNeil–Straumann 2002).

Monotonicity in the degrees of freedom

theorem ProbabilityTheory.Copula.integral_cos_rpow_ratio_lt {a ν μ : ℝ} (ha0 : 0 < a) (ha : a < Real.pi / 2) (hν : 0 < ν) (hνμ : ν < μ) : (∫ (θ : ℝ) in a..Real.pi / 2, Real.cos θ ^ μ) * ∫ (θ : ℝ) in 0..a, Real.cos θ ^ ν < (∫ (θ : ℝ) in a..Real.pi / 2, Real.cos θ ^ ν) * ∫ (θ : ℝ) in 0..a, Real.cos θ ^ μ

The key ratio inequality: for 0 < a < π/2 and 0 < ν < μ, ∫_a^{π/2} cos^μ · ∫_0^a cos^ν < ∫_a^{π/2} cos^ν · ∫_0^a cos^μ.

theorem ProbabilityTheory.Copula.studentTTailCoeff_strictAntiOn {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : StrictAntiOn (fun (ν : ℝ) => studentTTailCoeff ν r) (Set.Ioi 0)

Strict monotonicity in ν: for r ∈ (−1, 1), the tail-dependence coefficient λ(ν, r) of the t copula is strictly decreasing in the degrees of freedom ν > 0 (Embrechts–McNeil–Straumann 2002, Demarta–McNeil 2005).

Limits in the degrees of freedom

theorem ProbabilityTheory.Copula.integral_cos_rpow_ratio_le {a ν : ℝ} (ha0 : 0 < a) (ha : a ≤ Real.pi / 2) (hν : 0 < ν) : (∫ (θ : ℝ) in a..Real.pi / 2, Real.cos θ ^ ν) / ∫ (θ : ℝ) in 0..Real.pi / 2, Real.cos θ ^ ν ≤ (Real.pi - 2 * a) / a * (Real.cos a / Real.cos (a / 2)) ^ ν

An explicit exponential bound: for 0 < a ≤ π/2 and ν > 0, ∫_a^{π/2} cos^ν / ∫_0^{π/2} cos^ν ≤ ((π − 2a)/a) (cos a / cos (a/2))^ν.

theorem ProbabilityTheory.Copula.tendsto_studentTTailCoeff_atTop {r : ℝ} (hr : r < 1) : Filter.Tendsto (fun (ν : ℝ) => studentTTailCoeff ν r) Filter.atTop (nhds 0)

Gaussian limit: for r < 1, λ(ν, r) → 0 as ν → ∞, consistent with the tail independence of the Gaussian copula (the t law converges to the normal law as ν → ∞).

theorem ProbabilityTheory.Copula.tendsto_studentTTailCoeff_nhdsGT_zero (r : ℝ) : Filter.Tendsto (fun (ν : ℝ) => studentTTailCoeff ν r) (nhdsWithin 0 (Set.Ioi 0)) (nhds (1 - Real.arccos r / Real.pi))

Cauchy-type limit: λ(ν, r) → 1 − arccos(r)/π as ν → 0⁺.

theorem ProbabilityTheory.Copula.studentTTailCoeff_lt_limit {ν r : ℝ} (hν : 0 < ν) (hr : r ∈ Set.Ioo (-1) 1) : studentTTailCoeff ν r < 1 - Real.arccos r / Real.pi

For r ∈ (−1, 1) and ν > 0, λ(ν, r) < 1 − arccos(r)/π: the ν → 0⁺ limit is the strict supremum of the coefficient over the degrees of freedom.