← Mathematical handbook

theorem Papers.AnsariRockel2024.galambos_power_diagonal (δ : ℝ) (hδ : 0 < δ) : (Verification.galambos δ hδ).HasPowerDiagonal (2 - 2 ^ (-1 / δ))

theorem Papers.AnsariRockel2024.galambos_extremalCoefficient (δ : ℝ) (hδ : 0 < δ) : (Verification.galambos δ hδ).extremalCoefficient = 2 - 2 ^ (-1 / δ)

theorem Papers.AnsariRockel2024.galambos_tails (δ : ℝ) (hδ : 0 < δ) : (Verification.galambos δ hδ).HasLowerTailDependence 0 ∧ (Verification.galambos δ hδ).HasUpperTailDependence (2 ^ (-1 / δ))