← Copula mathematical handbook

Tail coefficients, Blomqvist's beta and Spearman's footrule of extreme-value copulas

The diagonal of a Pickands copula is t ^ (2 A(1/2)), so all diagonal-based quantities are explicit in A(1/2):

• upper tail dependence λ_U = 2 (1 - A(1/2)) (hasUpperTailDependence_pickandsCopula);
• lower tail dependence λ_L = 0, unless A(1/2) = 1/2 (i.e. C_A = M), where it is 1 (hasLowerTailDependence_pickandsCopula);
• Blomqvist's beta β = 2 ^ (2 (1 - A(1/2))) - 1 (blomqvistBeta_pickandsCopula);
• Spearman's footrule φ = 6 / (2 A(1/2) + 1) - 2 (spearmanFootrule_pickandsCopula).

The same statements for an arbitrary bivariate extreme-value copula, in terms of its Pickands function pickandsOf C, are the IsExtremeValue.*_pickandsOf versions.

References: G. Gudendorf and J. Segers, Extreme-value copulas (2010); H. Joe, Dependence Modeling with Copulas (2014).

theorem ProbabilityTheory.Copula.hasUpperTailDependence_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).HasUpperTailDependence (2 * (1 - A (1 / 2)))

Upper tail dependence of a Pickands copula: λ_U = 2 (1 - A(1/2)).

theorem ProbabilityTheory.Copula.hasLowerTailDependence_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).HasLowerTailDependence (if A (1 / 2) = 1 / 2 then 1 else 0)

Lower tail dependence of a Pickands copula: λ_L = 0 unless A(1/2) = 1/2 (C_A = M).

theorem ProbabilityTheory.Copula.blomqvistBeta_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).blomqvistBeta = 2 ^ (2 * (1 - A (1 / 2))) - 1

Blomqvist's beta of a Pickands copula: β = 2 ^ (2 (1 - A(1/2))) - 1.

theorem ProbabilityTheory.Copula.spearmanFootrule_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).spearmanFootrule = 6 / (2 * A (1 / 2) + 1) - 2

Spearman's footrule of a Pickands copula: φ = 6 / (2 A(1/2) + 1) - 2.

theorem ProbabilityTheory.Copula.IsExtremeValue.extremalCoefficient_eq_pickandsOf {C : Copula 2} (hC : C.IsExtremeValue) : C.extremalCoefficient = 2 * C.pickandsOf (1 / 2)

The extremal coefficient of an extreme-value copula is 2 A_C(1/2).

theorem ProbabilityTheory.Copula.IsExtremeValue.hasUpperTailDependence_pickandsOf {C : Copula 2} (hC : C.IsExtremeValue) : C.HasUpperTailDependence (2 * (1 - C.pickandsOf (1 / 2)))

λ_U = 2 (1 - A_C(1/2)) for every bivariate extreme-value copula.

theorem ProbabilityTheory.Copula.IsExtremeValue.blomqvistBeta_pickandsOf {C : Copula 2} (hC : C.IsExtremeValue) : C.blomqvistBeta = 2 ^ (2 * (1 - C.pickandsOf (1 / 2))) - 1

β = 2 ^ (2 (1 - A_C(1/2))) - 1 for every bivariate extreme-value copula.

theorem ProbabilityTheory.Copula.IsExtremeValue.spearmanFootrule_pickandsOf {C : Copula 2} (hC : C.IsExtremeValue) : C.spearmanFootrule = 6 / (2 * C.pickandsOf (1 / 2) + 1) - 2

φ = 6 / (2 A_C(1/2) + 1) - 2 for every bivariate extreme-value copula.

theorem ProbabilityTheory.Copula.IsExtremeValue.eq_comonotonic_iff_pickandsOf {C : Copula 2} (hC : C.IsExtremeValue) : C = comonotonic 2 ↔ C.pickandsOf (1 / 2) = 1 / 2

An extreme-value copula is M iff A_C(1/2) = 1/2.