← Copula mathematical handbook

Pickands functions of the classical extreme-value families

The existing extreme-value constructors of the library are identified as Pickands copulas, with their Pickands functions on [0,1]:

• independence: A ≡ 1; comonotonicity: A(t) = max(t, 1 - t);
• Gumbel–Hougaard (logistic), θ ≥ 1: A(t) = (t^θ + (1-t)^θ)^{1/θ} (gumbelPickands);
• Marshall–Olkin with the library's convention C(u,v) = min(u^α, v^β) u^{1-α} v^{1-β}: A(t) = max(1 - β t, 1 - α (1 - t)) (marshallOlkinPickands); Cuadras–Augé is the case α = β;
• Tawn's asymmetric logistic C(u,v) = u^{1-α} v^{1-β} exp(-((α x)^θ + (β y)^θ)^{1/θ}) (x = -log u, y = -log v): A(t) = (1-α)(1-t) + (1-β) t + ((α(1-t))^θ + (β t)^θ)^{1/θ} (tawnPickands).

In each case the Pickands property (in particular convexity) is obtained from the general converse theorem IsExtremeValue.isPickandsFunction_pickandsOf, since the families are known to be max-stable copulas.

(With the opposite labelling of the coordinates, the Marshall–Olkin function reads max(1 - α t, 1 - β (1 - t)) as in Gudendorf–Segers (2010).)

References: G. Gudendorf and J. Segers, Extreme-value copulas (2010); H. Joe, Dependence Modeling with Copulas (2014); J. A. Tawn, Bivariate extreme value theory: models and estimation (1988).

theorem ProbabilityTheory.Copula.IsPickandsFunction.congr {A B : ℝ → ℝ} (hA : IsPickandsFunction A) (h : Set.EqOn A B (Set.Icc 0 1)) : IsPickandsFunction B

Pickands functions may be changed off [0,1].

theorem ProbabilityTheory.Copula.IsExtremeValue.eq_pickandsCopula_of_eqOn {C : Copula 2} (hC : C.IsExtremeValue) {B : ℝ → ℝ} (hB : IsPickandsFunction B) (h : Set.EqOn C.pickandsOf B (Set.Icc 0 1)) : C = pickandsCopula B hB

An extreme-value copula is the Pickands copula of any function agreeing with A_C on [0,1].

theorem ProbabilityTheory.Copula.pickandsOf_independence : Set.EqOn (independence 2).pickandsOf (fun (x : ℝ) => 1) (Set.Icc 0 1)

theorem ProbabilityTheory.Copula.pickandsOf_comonotonic : Set.EqOn (comonotonic 2).pickandsOf (fun (t : ℝ) => max t (1 - t)) (Set.Icc 0 1)

Gumbel–Hougaard

noncomputable def ProbabilityTheory.Copula.gumbelPickands (θ t : ℝ) : ℝ

The logistic Pickands function (t^θ + (1-t)^θ)^{1/θ}.

Equations

• ProbabilityTheory.Copula.gumbelPickands θ t = (t ^ θ + (1 - t) ^ θ) ^ θ⁻¹

theorem ProbabilityTheory.Copula.pickandsOf_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : Set.EqOn (gumbel θ hθ).pickandsOf (gumbelPickands θ) (Set.Icc 0 1)

theorem ProbabilityTheory.Copula.isPickandsFunction_gumbelPickands (θ : ℝ) (hθ : 1 ≤ θ) : IsPickandsFunction (gumbelPickands θ)

The logistic function is a Pickands function for θ ≥ 1.

theorem ProbabilityTheory.Copula.gumbel_eq_pickandsCopula (θ : ℝ) (hθ : 1 ≤ θ) : gumbel θ hθ = pickandsCopula (gumbelPickands θ) ⋯

The Gumbel–Hougaard copula is the Pickands copula of the logistic function.

Marshall–Olkin and Cuadras–Augé

noncomputable def ProbabilityTheory.Copula.marshallOlkinPickands (α β t : ℝ) : ℝ

The Marshall–Olkin Pickands function max(1 - β t, 1 - α (1 - t)).

Equations

• ProbabilityTheory.Copula.marshallOlkinPickands α β t = max (1 - β * t) (1 - α * (1 - t))

theorem ProbabilityTheory.Copula.pickandsOf_marshallOlkin (α β : ↑unitInterval) : Set.EqOn (marshallOlkin α β).pickandsOf (marshallOlkinPickands ↑α ↑β) (Set.Icc 0 1)

theorem ProbabilityTheory.Copula.isPickandsFunction_marshallOlkinPickands (α β : ↑unitInterval) : IsPickandsFunction (marshallOlkinPickands ↑α ↑β)

theorem ProbabilityTheory.Copula.marshallOlkin_eq_pickandsCopula (α β : ↑unitInterval) : marshallOlkin α β = pickandsCopula (marshallOlkinPickands ↑α ↑β) ⋯

The Marshall–Olkin copula is the Pickands copula of max(1 - β t, 1 - α (1 - t)).

theorem ProbabilityTheory.Copula.cuadrasAuge_eq_pickandsCopula (α : ↑unitInterval) : cuadrasAuge α = pickandsCopula (marshallOlkinPickands ↑α ↑α) ⋯

The Cuadras–Augé copula is the Pickands copula of 1 - α min(t, 1 - t).

theorem ProbabilityTheory.Copula.marshallOlkinPickands_self (α t : ℝ) (hα : 0 ≤ α) : marshallOlkinPickands α α t = 1 - α * min t (1 - t)

Tawn's asymmetric logistic model

noncomputable def ProbabilityTheory.Copula.tawnPickands (θ α β t : ℝ) : ℝ

Tawn's asymmetric logistic Pickands function (1-α)(1-t) + (1-β) t + ((α(1-t))^θ + (β t)^θ)^{1/θ}.

Equations

• ProbabilityTheory.Copula.tawnPickands θ α β t = (1 - α) * (1 - t) + (1 - β) * t + ((α * (1 - t)) ^ θ + (β * t) ^ θ) ^ θ⁻¹

theorem ProbabilityTheory.Copula.pickandsOf_tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : Set.EqOn (tawn θ hθ α β).pickandsOf (tawnPickands θ ↑α ↑β) (Set.Icc 0 1)

theorem ProbabilityTheory.Copula.isPickandsFunction_tawnPickands (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : IsPickandsFunction (tawnPickands θ ↑α ↑β)

theorem ProbabilityTheory.Copula.tawn_eq_pickandsCopula (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : tawn θ hθ α β = pickandsCopula (tawnPickands θ ↑α ↑β) ⋯

Tawn's asymmetric logistic copula is the Pickands copula of tawnPickands.