← Mathematical handbook

Extremal coefficients and diagonal sections of extreme-value copulas

Max-stability alone implies a power diagonal. This yields the extremal coefficient in [1,2] and both tail limits, without requiring a density or a Pickands representation. See Gudendorf and Segers, Extreme-Value Copulas, §4.

theorem ProbabilityTheory.Copula.IsExtremeValue.diagonal_unitPower {C : Copula 2} (hC : C.IsExtremeValue) (u : ↑unitInterval) (r : ℝ) (hr : 0 < r) : C.diagonal (unitPower u r ⋯) = C.diagonal u ^ r

theorem ProbabilityTheory.Copula.IsExtremeValue.exists_hasPowerDiagonal {C : Copula 2} (hC : C.IsExtremeValue) : ∃ (κ : ℝ), C.HasPowerDiagonal κ

Every bivariate extreme-value copula has a power diagonal on the closed interval.

noncomputable def ProbabilityTheory.Copula.extremalCoefficient (C : Copula 2) : ℝ

The diagonal exponent, evaluated at one half. For extreme-value copulas it is the usual extremal coefficient 2 A(1/2).

Equations

• C.extremalCoefficient = Real.log (C.diagonal ProbabilityTheory.Copula.unitHalf) / Real.log (1 / 2)

theorem ProbabilityTheory.Copula.HasPowerDiagonal.extremalCoefficient_eq {C : Copula 2} {κ : ℝ} (h : C.HasPowerDiagonal κ) : C.extremalCoefficient = κ

theorem ProbabilityTheory.Copula.IsExtremeValue.hasPowerDiagonal {C : Copula 2} (hC : C.IsExtremeValue) : C.HasPowerDiagonal C.extremalCoefficient

theorem ProbabilityTheory.Copula.IsExtremeValue.extremalCoefficient_mem_Icc {C : Copula 2} (hC : C.IsExtremeValue) : C.extremalCoefficient ∈ Set.Icc 1 2

theorem ProbabilityTheory.Copula.IsExtremeValue.hasUpperTailDependence {C : Copula 2} (hC : C.IsExtremeValue) : C.HasUpperTailDependence (2 - C.extremalCoefficient)

theorem ProbabilityTheory.Copula.IsExtremeValue.extremalCoefficient_eq_one_iff {C : Copula 2} (hC : C.IsExtremeValue) : C.extremalCoefficient = 1 ↔ C = comonotonic 2

theorem ProbabilityTheory.Copula.IsExtremeValue.hasLowerTailDependence_zero {C : Copula 2} (hC : C.IsExtremeValue) (hne : C ≠ comonotonic 2) : C.HasLowerTailDependence 0

All extreme-value copulas except comonotonicity have independent lower tails.

theorem ProbabilityTheory.Copula.LowerOrthantLE.extremalCoefficient_antitone {C D : Copula 2} (h : C.LowerOrthantLE D) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) : D.extremalCoefficient ≤ C.extremalCoefficient

Greater concordance gives a smaller extremal coefficient.

theorem ProbabilityTheory.Copula.IsExtremeValue.hasUpperTailDependence_one_iff {C : Copula 2} (hC : C.IsExtremeValue) : C.HasUpperTailDependence 1 ↔ C = comonotonic 2