← Copula mathematical handbook

Pickands dependence functions and bivariate extreme-value copulas

A Pickands dependence function is a convex function A : [0,1] → ℝ with max(t, 1 - t) ≤ A(t) ≤ 1. The associated stable tail dependence function is ℓ_A(x,y) = (x + y) A(y / (x + y)) on [0,∞)², and the Pickands copula is

C_A(u,v) = exp(log(uv) A(log v / log(uv))) = exp(-ℓ_A(-log u, -log v))

for u, v ∈ (0,1], extended by zero on the two lower edges.

Main results:

• pickandsCopula A hA: C_A is a copula (IsPickandsFunction A suffices). The proof of 2-increasingness is the standard one: ℓ_A is positively homogeneous, nondecreasing in each variable and submodular (from the chord-slope monotonicity of the convex perspective r ↦ ℓ_A(1,r)), and exp ∘ (-ℓ_A) is then supermodular because exp is convex and increasing.
• cdf_pickandsCopula_eq_exp: the classical formula exp(log(uv) A(log v / log(uv))).
• isExtremeValue_pickandsCopula: C_A is max-stable.
• pickandsCopula_const_one: A ≡ 1 gives Π; pickandsCopula_max: A = max(t,1-t) gives M.
• pickandsCopula_eq_iff: A ↦ C_A is injective on [0,1]; pickandsCopula_lowerOrthantLE_iff: A ≤ B on [0,1] iff C_B ≤ C_A pointwise.
• isPQD_pickandsCopula: every Pickands copula is positively quadrant dependent.
• hasPowerDiagonal_pickandsCopula: the diagonal is t^{2A(1/2)}, so the extremal coefficient is 2A(1/2); pickandsCopula_eq_comonotonic_iff: C_A = M iff A(1/2) = 1/2.

The converse (every bivariate extreme-value copula is a Pickands copula) is in Copula.ExtremeValue.PickandsConverse.

References: J. Pickands, Multivariate extreme value distributions (1981); G. Gudendorf and J. Segers, Extreme-value copulas, in Copula Theory and Its Applications (2010); H. Joe, Dependence Modeling with Copulas (2014); F. Durante and C. Sempi, Principles of Copula Theory (2016).

structure ProbabilityTheory.Copula.IsPickandsFunction (A : ℝ → ℝ) : Prop

A Pickands dependence function: convex on [0,1] with max(t, 1 - t) ≤ A(t) ≤ 1 there. Values outside [0,1] are irrelevant.

• convexOn : ConvexOn ℝ (Set.Icc 0 1) A
• le_one (t : ℝ) : t ∈ Set.Icc 0 1 → A t ≤ 1
• max_le (t : ℝ) : t ∈ Set.Icc 0 1 → max t (1 - t) ≤ A t

noncomputable def ProbabilityTheory.Copula.pickandsTail (A : ℝ → ℝ) (x y : ℝ) : ℝ

The stable tail dependence function ℓ_A(x,y) = (x + y) A(y / (x + y)) of a Pickands function (with ℓ_A(0,0) = 0).

Equations

• ProbabilityTheory.Copula.pickandsTail A x y = (x + y) * A (y / (x + y))

theorem ProbabilityTheory.Copula.pickands_ratio_mem {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : y / (x + y) ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.IsPickandsFunction.apply_zero {A : ℝ → ℝ} (hA : IsPickandsFunction A) : A 0 = 1

theorem ProbabilityTheory.Copula.IsPickandsFunction.apply_one {A : ℝ → ℝ} (hA : IsPickandsFunction A) : A 1 = 1

theorem ProbabilityTheory.Copula.IsPickandsFunction.half_le {A : ℝ → ℝ} (hA : IsPickandsFunction A) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : 1 / 2 ≤ A t

theorem ProbabilityTheory.Copula.IsPickandsFunction.pos {A : ℝ → ℝ} (hA : IsPickandsFunction A) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : 0 < A t

theorem ProbabilityTheory.Copula.IsPickandsFunction.comp_one_sub {A : ℝ → ℝ} (hA : IsPickandsFunction A) : IsPickandsFunction fun (t : ℝ) => A (1 - t)

The reflected function t ↦ A(1 - t) (the Pickands function of the transposed copula).

theorem ProbabilityTheory.Copula.IsPickandsFunction.eq_max_iff {A : ℝ → ℝ} (hA : IsPickandsFunction A) : A (1 / 2) = 1 / 2 ↔ Set.EqOn A (fun (t : ℝ) => max t (1 - t)) (Set.Icc 0 1)

A Pickands function lies below the chord max(t, 1-t) iff it touches it at 1/2.

theorem ProbabilityTheory.Copula.pickandsTail_smul (A : ℝ → ℝ) {s : ℝ} (hs : s ≠ 0) (x y : ℝ) : pickandsTail A (s * x) (s * y) = s * pickandsTail A x y

theorem ProbabilityTheory.Copula.pickandsTail_zero_left {A : ℝ → ℝ} (hA : IsPickandsFunction A) (y : ℝ) : pickandsTail A 0 y = y

theorem ProbabilityTheory.Copula.pickandsTail_zero_right {A : ℝ → ℝ} (hA : IsPickandsFunction A) (x : ℝ) : pickandsTail A x 0 = x

theorem ProbabilityTheory.Copula.pickandsTail_le_add {A : ℝ → ℝ} (hA : IsPickandsFunction A) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : pickandsTail A x y ≤ x + y

theorem ProbabilityTheory.Copula.max_le_pickandsTail {A : ℝ → ℝ} (hA : IsPickandsFunction A) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : max x y ≤ pickandsTail A x y

theorem ProbabilityTheory.Copula.pickandsTail_nonneg {A : ℝ → ℝ} (hA : IsPickandsFunction A) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : 0 ≤ pickandsTail A x y

theorem ProbabilityTheory.Copula.pickandsTail_swap (A : ℝ → ℝ) (x y : ℝ) : pickandsTail A x y = pickandsTail (fun (t : ℝ) => A (1 - t)) y x

theorem ProbabilityTheory.Copula.convexOn_pickandsTail_one {A : ℝ → ℝ} (hA : IsPickandsFunction A) : ConvexOn ℝ (Set.Ici 0) fun (r : ℝ) => pickandsTail A 1 r

The perspective r ↦ ℓ_A(1, r) is convex on [0, ∞).

theorem ProbabilityTheory.Copula.pickandsTail_one_mono {A : ℝ → ℝ} (hA : IsPickandsFunction A) {r r' : ℝ} (hr : 0 ≤ r) (hrr : r ≤ r') : pickandsTail A 1 r ≤ pickandsTail A 1 r'

theorem ProbabilityTheory.Copula.pickandsTail_mono_right {A : ℝ → ℝ} (hA : IsPickandsFunction A) {x y y' : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hyy : y ≤ y') : pickandsTail A x y ≤ pickandsTail A x y'

ℓ_A is nondecreasing in its second variable.

theorem ProbabilityTheory.Copula.pickandsTail_mono_left {A : ℝ → ℝ} (hA : IsPickandsFunction A) {x x' y : ℝ} (hx : 0 ≤ x) (hxx : x ≤ x') (hy : 0 ≤ y) : pickandsTail A x y ≤ pickandsTail A x' y

ℓ_A is nondecreasing in its first variable.

theorem ProbabilityTheory.Copula.pickandsTail_submodular {A : ℝ → ℝ} (hA : IsPickandsFunction A) {x x' y y' : ℝ} (hx : 0 ≤ x) (hxx : x ≤ x') (hy : 0 ≤ y) (hyy : y ≤ y') : pickandsTail A x y + pickandsTail A x' y' ≤ pickandsTail A x y' + pickandsTail A x' y

ℓ_A is submodular on [0,∞)²: for x ≤ x', y ≤ y', ℓ(x,y) + ℓ(x',y') ≤ ℓ(x,y') + ℓ(x',y).

theorem ProbabilityTheory.Copula.pickandsTail_le_of_le {A B : ℝ → ℝ} (h : ∀ t ∈ Set.Icc 0 1, A t ≤ B t) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : pickandsTail A x y ≤ pickandsTail B x y

noncomputable def ProbabilityTheory.Copula.pickandsCDF (A : ℝ → ℝ) (u v : ↑unitInterval) : ℝ

The Pickands CDF formula exp(-ℓ_A(-log u, -log v)), zero on the lower edges.

Equations

• ProbabilityTheory.Copula.pickandsCDF A u v = if u = 0 ∨ v = 0 then 0 else Real.exp (-ProbabilityTheory.Copula.pickandsTail A (-Real.log ↑u) (-Real.log ↑v))

theorem ProbabilityTheory.Copula.pickandsCDF_nonneg (A : ℝ → ℝ) (u v : ↑unitInterval) : 0 ≤ pickandsCDF A u v

theorem ProbabilityTheory.Copula.pickandsCDF_zero_left (A : ℝ → ℝ) (v : ↑unitInterval) : pickandsCDF A 0 v = 0

theorem ProbabilityTheory.Copula.pickandsCDF_zero_right (A : ℝ → ℝ) (u : ↑unitInterval) : pickandsCDF A u 0 = 0

theorem ProbabilityTheory.Copula.pickandsCDF_one_left {A : ℝ → ℝ} (hA : IsPickandsFunction A) (v : ↑unitInterval) : pickandsCDF A 1 v = ↑v

theorem ProbabilityTheory.Copula.pickandsCDF_one_right {A : ℝ → ℝ} (hA : IsPickandsFunction A) (u : ↑unitInterval) : pickandsCDF A u 1 = ↑u

theorem ProbabilityTheory.Copula.pickandsCDF_mono {A : ℝ → ℝ} (hA : IsPickandsFunction A) {u u' v v' : ↑unitInterval} (hu : u ≤ u') (hv : v ≤ v') : pickandsCDF A u v ≤ pickandsCDF A u' v'

theorem ProbabilityTheory.Copula.pickandsCDF_rect {A : ℝ → ℝ} (hA : IsPickandsFunction A) {a b c e : ↑unitInterval} (hab : a ≤ b) (hce : c ≤ e) : 0 ≤ pickandsCDF A b e - pickandsCDF A a e - pickandsCDF A b c + pickandsCDF A a c

noncomputable def ProbabilityTheory.Copula.pickandsCopula (A : ℝ → ℝ) (hA : IsPickandsFunction A) : Copula 2

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

Equations

• ProbabilityTheory.Copula.pickandsCopula A hA = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.pickandsCDF A (u 0) (u 1)) ⋯

theorem ProbabilityTheory.Copula.cdf_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) (u : Fin 2 → ↑unitInterval) : (pickandsCopula A hA).cdf u = pickandsCDF A (u 0) (u 1)

theorem ProbabilityTheory.Copula.cdf_pickandsCopula_two {A : ℝ → ℝ} (hA : IsPickandsFunction A) (u v : ↑unitInterval) : (pickandsCopula A hA).cdf ![u, v] = pickandsCDF A u v

theorem ProbabilityTheory.Copula.cdf_pickandsCopula_eq_exp {A : ℝ → ℝ} (hA : IsPickandsFunction A) {u v : ↑unitInterval} (hu : u ≠ 0) (hv : v ≠ 0) : (pickandsCopula A hA).cdf ![u, v] = Real.exp (Real.log (↑u * ↑v) * A (Real.log ↑v / Real.log (↑u * ↑v)))

The classical Pickands formula C_A(u,v) = exp(log(uv) A(log v / log(uv))) on (0,1]².

theorem ProbabilityTheory.Copula.isExtremeValue_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).IsExtremeValue

Pickands copulas are extreme-value copulas (max-stable).

noncomputable def ProbabilityTheory.Copula.expNegUnit (s : ℝ) : ↑unitInterval

The point exp(-max(s, 0)) of the unit interval.

Equations

• ProbabilityTheory.Copula.expNegUnit s = ⟨Real.exp (-max s 0), ⋯⟩

@[simp]

theorem ProbabilityTheory.Copula.coe_expNegUnit (s : ℝ) : ↑(expNegUnit s) = Real.exp (-max s 0)

theorem ProbabilityTheory.Copula.expNegUnit_ne_zero (s : ℝ) : expNegUnit s ≠ 0

theorem ProbabilityTheory.Copula.neg_log_expNegUnit (s : ℝ) : -Real.log ↑(expNegUnit s) = max s 0

theorem ProbabilityTheory.Copula.cdf_pickandsCopula_expNegUnit {A : ℝ → ℝ} (hA : IsPickandsFunction A) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (pickandsCopula A hA).cdf ![expNegUnit (1 - t), expNegUnit t] = Real.exp (-A t)

Evaluation of C_A on the curve (e^{-(1-t)}, e^{-t}) recovers A.

theorem ProbabilityTheory.Copula.isPickandsFunction_const_one : IsPickandsFunction fun (x : ℝ) => 1

The constant Pickands function 1.

theorem ProbabilityTheory.Copula.pickandsCopula_const_one : pickandsCopula (fun (x : ℝ) => 1) isPickandsFunction_const_one = independence 2

A ≡ 1 gives the independence copula.

theorem ProbabilityTheory.Copula.isPickandsFunction_max : IsPickandsFunction fun (t : ℝ) => max t (1 - t)

The lower boundary max(t, 1 - t) is a Pickands function.

theorem ProbabilityTheory.Copula.pickandsTail_max {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : pickandsTail (fun (t : ℝ) => max t (1 - t)) x y = max x y

theorem ProbabilityTheory.Copula.pickandsCopula_max : pickandsCopula (fun (t : ℝ) => max t (1 - t)) isPickandsFunction_max = comonotonic 2

A = max(t, 1 - t) gives the comonotonicity copula M.

theorem ProbabilityTheory.Copula.isPQD_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).IsPQD

Every Pickands copula is positively quadrant dependent (A ≤ 1).

theorem ProbabilityTheory.Copula.pickandsCopula_lowerOrthantLE {A B : ℝ → ℝ} (hA : IsPickandsFunction A) (hB : IsPickandsFunction B) (h : ∀ t ∈ Set.Icc 0 1, A t ≤ B t) : (pickandsCopula B hB).LowerOrthantLE (pickandsCopula A hA)

Pointwise order of Pickands functions reverses the pointwise order of copulas.

theorem ProbabilityTheory.Copula.pickandsCopula_lowerOrthantLE_iff {A B : ℝ → ℝ} (hA : IsPickandsFunction A) (hB : IsPickandsFunction B) : (pickandsCopula B hB).LowerOrthantLE (pickandsCopula A hA) ↔ ∀ t ∈ Set.Icc 0 1, A t ≤ B t

A ≤ B on [0,1] if and only if C_B ≤ C_A pointwise.

theorem ProbabilityTheory.Copula.pickandsCopula_eq_iff {A B : ℝ → ℝ} (hA : IsPickandsFunction A) (hB : IsPickandsFunction B) : pickandsCopula A hA = pickandsCopula B hB ↔ Set.EqOn A B (Set.Icc 0 1)

A ↦ C_A is injective: two Pickands copulas agree iff the functions agree on [0,1].

theorem ProbabilityTheory.Copula.hasPowerDiagonal_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).HasPowerDiagonal (2 * A (1 / 2))

The diagonal of C_A is t ^ (2 A(1/2)).

theorem ProbabilityTheory.Copula.extremalCoefficient_pickandsCopula {A : ℝ → ℝ} (hA : IsPickandsFunction A) : (pickandsCopula A hA).extremalCoefficient = 2 * A (1 / 2)

The extremal coefficient of C_A is 2 A(1/2).

theorem ProbabilityTheory.Copula.pickandsCopula_eq_comonotonic_iff {A : ℝ → ℝ} (hA : IsPickandsFunction A) : pickandsCopula A hA = comonotonic 2 ↔ A (1 / 2) = 1 / 2

C_A = M iff A(1/2) = 1/2 (iff A = max(t, 1-t) on [0,1]).

theorem ProbabilityTheory.Copula.pickandsCopula_eq_independence_iff {A : ℝ → ℝ} (hA : IsPickandsFunction A) : pickandsCopula A hA = independence 2 ↔ Set.EqOn A (fun (x : ℝ) => 1) (Set.Icc 0 1)

C_A = Π iff A ≡ 1 on [0,1].