← Mathematical handbook

Canonical Pickands functions and exact extreme-value CDF order

The function is recovered from an actual max-stable copula. No density, smoothness, or pre-assumed ordering of generators is required.

noncomputable def Verification.unitNegExp (x : ℝ) (hx : 0 ≤ x) : ↑unitInterval

Equations

• Verification.unitNegExp x hx = ⟨Real.exp (-x), ⋯⟩

noncomputable def Verification.pickandsRay (t : ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• Verification.pickandsRay t = ![Verification.unitNegExp ((1 - ↑t) / 2) ⋯, Verification.unitNegExp (↑t / 2) ⋯]

theorem Verification.pickandsRay_cdf_pos (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) : 0 < C.cdf (pickandsRay t)

noncomputable def Verification.copulaPickands (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) : ℝ

The usual Pickands function, evaluated on a ray with logarithmic radius one half.

Equations

• Verification.copulaPickands C t = -2 * Real.log (C.cdf (Verification.pickandsRay t))

theorem Verification.extremeValue_exp_coordinates (C : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : 0 < x + y) : C.cdf ![unitNegExp x hx, unitNegExp y hy] = Real.exp (-(x + y) * copulaPickands C ⟨y / (x + y), ⋯⟩)

theorem Verification.copulaPickands_zero (C : ProbabilityTheory.Copula 2) : copulaPickands C 0 = 1

theorem Verification.copulaPickands_one (C : ProbabilityTheory.Copula 2) : copulaPickands C 1 = 1

theorem Verification.extremeValue_lowerOrthant_iff_pickands (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) : C.LowerOrthantLE D ↔ ∀ (t : ↑unitInterval), copulaPickands D t ≤ copulaPickands C t

Theorem 3.4(i)-(ii), with the Pickands function extracted from max-stability.

theorem Verification.extremeValue_lowerOrthant_iff_pickands_interior (C D : ProbabilityTheory.Copula 2) (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) : C.LowerOrthantLE D ↔ ∀ (t : ↑unitInterval), 0 < t → t < 1 → copulaPickands D t ≤ copulaPickands C t

The open-interval formulation in the paper is equivalent, because both endpoints equal one.