← Mathematical handbook

theorem Papers.AnsariRockel2024.joeExtremeValue_pickands_interior (δ : ℝ) (hδ : 0 < δ) (α β t : ↑unitInterval) (hα : 0 < ↑α) (hβ : 0 < ↑β) (ht : ↑t ∈ Set.Ioo 0 1) : Verification.copulaPickands (Verification.joeExtremeValue δ hδ α β) t = 1 - ((↑α * (1 - ↑t)) ^ (-δ) + (↑β * ↑t) ^ (-δ)) ^ (-1 / δ)

theorem Papers.AnsariRockel2024.joeExtremeValue_pickands_zero_weight (δ : ℝ) (hδ : 0 < δ) (α β t : ↑unitInterval) (h : α = 0 ∨ β = 0) : Verification.copulaPickands (Verification.joeExtremeValue δ hδ α β) t = 1

theorem Papers.AnsariRockel2024.joeExtremeValue_pickands_endpoints (δ : ℝ) (hδ : 0 < δ) (α β : ↑unitInterval) : Verification.copulaPickands (Verification.joeExtremeValue δ hδ α β) 0 = 1 ∧ Verification.copulaPickands (Verification.joeExtremeValue δ hδ α β) 1 = 1