← Copula mathematical handbook

Every bivariate extreme-value copula is a Pickands copula

For a bivariate copula C define A_C(t) = -log C(e^{-(1-t)}, e^{-t}) (pickandsOf C). If C is max-stable (IsExtremeValue), then A_C is a Pickands dependence function and C = C_{A_C} (IsExtremeValue.eq_pickandsCopula). Hence the bivariate extreme-value copulas are exactly the Pickands copulas (isExtremeValue_iff_exists_pickands), every such copula is PQD, and the pointwise order of extreme-value copulas is the reversed order of their Pickands functions.

Proof of convexity of A_C (no spectral measure is needed). Put ℓ(x,y) = -log C(e^{-x}, e^{-y}) on [0,∞)². Max-stability makes ℓ positively homogeneous, so C(e^{-εx}, e^{-εy}) = exp(-ε ℓ(x,y)); 2-increasingness of C at scale ε and ε → 0 give submodularity of ℓ (evTail_submodular). Applied to the rectangle with corners (1-c, c) and λ(1-c, λc) this is a three-point convexity inequality for A_C around every c ∈ (0,1) with arbitrarily close points (pickandsOf_local), and a continuous function with this local property is convex (convexOn_Icc_of_local, an argmax argument).

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

theorem ProbabilityTheory.Copula.convexOn_Icc_of_local {f : ℝ → ℝ} {a b : ℝ} (hf : ContinuousOn f (Set.Icc a b)) (hloc : ∀ c ∈ Set.Ioo a b, ∀ ε > 0, ∃ (p : ℝ) (q : ℝ), c - ε < p ∧ p < c ∧ c < q ∧ q < c + ε ∧ (q - p) * f c ≤ (q - c) * f p + (c - p) * f q) : ConvexOn ℝ (Set.Icc a b) f

A continuous function on [a,b] which satisfies, around every interior point and at every scale, some three-point convexity inequality, is convex on [a,b].

noncomputable def ProbabilityTheory.Copula.evTail (C : Copula 2) (x y : ℝ) : ℝ

The (negative log of the) copula on the exponential scale: ℓ_C(x,y) = -log C(e^{-x}, e^{-y}) for x, y ≥ 0.

Equations

• C.evTail x y = -Real.log (C.cdf ![ProbabilityTheory.Copula.expNegUnit x, ProbabilityTheory.Copula.expNegUnit y])

noncomputable def ProbabilityTheory.Copula.pickandsOf (C : Copula 2) (t : ℝ) : ℝ

The Pickands function of a bivariate copula: A_C(t) = -log C(e^{-(1-t)}, e^{-t}).

Equations

• C.pickandsOf t = C.evTail (1 - t) t

theorem ProbabilityTheory.Copula.continuous_expNegUnit : Continuous expNegUnit

theorem ProbabilityTheory.Copula.expNegUnit_zero : expNegUnit 0 = 1

theorem ProbabilityTheory.Copula.expNegUnit_neg_log {u : ↑unitInterval} (hu : u ≠ 0) : expNegUnit (-Real.log ↑u) = u

theorem ProbabilityTheory.Copula.IsExtremeValue.cdf_pos {C : Copula 2} (hC : C.IsExtremeValue) {u v : ↑unitInterval} (hu : u ≠ 0) (hv : v ≠ 0) : 0 < C.cdf ![u, v]

Extreme-value copulas are positive on (0,1]².

theorem ProbabilityTheory.Copula.IsExtremeValue.evTail_exp {C : Copula 2} (hC : C.IsExtremeValue) (x y : ℝ) : Real.exp (-C.evTail x y) = C.cdf ![expNegUnit x, expNegUnit y]

theorem ProbabilityTheory.Copula.IsExtremeValue.evTail_smul {C : Copula 2} (hC : C.IsExtremeValue) {s : ℝ} (hs : 0 < s) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : C.evTail (s * x) (s * y) = s * C.evTail x y

Positive homogeneity of ℓ_C, from max-stability.

theorem ProbabilityTheory.Copula.IsExtremeValue.evTail_zero_right (C : Copula 2) {x : ℝ} (hx : 0 ≤ x) : C.evTail x 0 = x

theorem ProbabilityTheory.Copula.IsExtremeValue.evTail_zero_left (C : Copula 2) {y : ℝ} (hy : 0 ≤ y) : C.evTail 0 y = y

theorem ProbabilityTheory.Copula.IsExtremeValue.max_le_evTail {C : Copula 2} (hC : C.IsExtremeValue) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : max x y ≤ C.evTail x y

The Fréchet upper bound: max x y ≤ ℓ_C(x,y).

theorem ProbabilityTheory.Copula.IsExtremeValue.evTail_submodular {C : Copula 2} (hC : C.IsExtremeValue) {x x' y y' : ℝ} (hx : 0 ≤ x) (hxx : x ≤ x') (hy : 0 ≤ y) (hyy : y ≤ y') : C.evTail x y + C.evTail x' y' ≤ C.evTail x y' + C.evTail x' y

Submodularity of ℓ_C on [0,∞)².

theorem ProbabilityTheory.Copula.IsExtremeValue.continuous_pickandsOf {C : Copula 2} (hC : C.IsExtremeValue) : Continuous C.pickandsOf

theorem ProbabilityTheory.Copula.IsExtremeValue.pickandsOf_zero (C : Copula 2) : C.pickandsOf 0 = 1

theorem ProbabilityTheory.Copula.IsExtremeValue.pickandsOf_one (C : Copula 2) : C.pickandsOf 1 = 1

theorem ProbabilityTheory.Copula.IsExtremeValue.evTail_eq_mul_pickandsOf {C : Copula 2} (hC : C.IsExtremeValue) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : C.evTail x y = (x + y) * C.pickandsOf (y / (x + y))

Scaling ℓ_C along a ray in terms of A_C.

theorem ProbabilityTheory.Copula.IsExtremeValue.pickandsOf_local {C : Copula 2} (hC : C.IsExtremeValue) {c : ℝ} (hc : c ∈ Set.Ioo 0 1) {ε : ℝ} (hε : 0 < ε) : ∃ (p : ℝ) (q : ℝ), c - ε < p ∧ p < c ∧ c < q ∧ q < c + ε ∧ (q - p) * C.pickandsOf c ≤ (q - c) * C.pickandsOf p + (c - p) * C.pickandsOf q

The local three-point convexity inequality of A_C around c ∈ (0,1).

theorem ProbabilityTheory.Copula.IsExtremeValue.isPickandsFunction_pickandsOf {C : Copula 2} (hC : C.IsExtremeValue) : IsPickandsFunction C.pickandsOf

The Pickands function of a bivariate extreme-value copula is a Pickands dependence function.

theorem ProbabilityTheory.Copula.IsExtremeValue.eq_pickandsCopula {C : Copula 2} (hC : C.IsExtremeValue) : C = pickandsCopula C.pickandsOf ⋯

Pickands representation. Every bivariate extreme-value copula is the Pickands copula of its Pickands function A_C(t) = -log C(e^{-(1-t)}, e^{-t}).

theorem ProbabilityTheory.Copula.pickandsOf_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : Set.EqOn (pickandsCopula A hA).pickandsOf A (Set.Icc 0 1)

On [0,1], the Pickands function of C_A is A.

theorem ProbabilityTheory.Copula.isExtremeValue_iff_exists_pickands (C : Copula 2) : C.IsExtremeValue ↔ ∃ (A : ℝ → ℝ) (hA : IsPickandsFunction A), C = pickandsCopula A hA

The bivariate extreme-value copulas are exactly the Pickands copulas.

theorem ProbabilityTheory.Copula.IsExtremeValue.isPQD {C : Copula 2} (hC : C.IsExtremeValue) : C.IsPQD

Every bivariate extreme-value copula is positively quadrant dependent.

theorem ProbabilityTheory.Copula.IsExtremeValue.lowerOrthantLE_iff {C D : Copula 2} (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) : C.LowerOrthantLE D ↔ ∀ t ∈ Set.Icc 0 1, D.pickandsOf t ≤ C.pickandsOf t

For extreme-value copulas, C ≤ D pointwise iff A_D ≤ A_C on [0,1].

theorem ProbabilityTheory.Copula.IsExtremeValue.eq_iff {C D : Copula 2} (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) : C = D ↔ Set.EqOn C.pickandsOf D.pickandsOf (Set.Icc 0 1)

Two extreme-value copulas coincide iff their Pickands functions agree on [0,1].