← Mathematical handbook

theorem Papers.AnsariRockel2024.joeExtremeValue_extremalCoefficient (δ : ℝ) (hδ : 0 < δ) (α β : ↑unitInterval) (hα : 0 < ↑α) (hβ : 0 < ↑β) : (Verification.joeExtremeValue δ hδ α β).extremalCoefficient = 2 - (↑α ^ (-δ) + ↑β ^ (-δ)) ^ (-1 / δ)

theorem Papers.AnsariRockel2024.joeExtremeValue_tails (δ : ℝ) (hδ : 0 < δ) (α β : ↑unitInterval) : (Verification.joeExtremeValue δ hδ α β).HasLowerTailDependence 0 ∧ (Verification.joeExtremeValue δ hδ α β).HasUpperTailDependence (if α = 0 ∨ β = 0 then 0 else (↑α ^ (-δ) + ↑β ^ (-δ)) ^ (-1 / δ))