← Mathematical handbook

theorem Papers.AnsariRockel2024.bb5_extremalCoefficient (θ δ : ℝ) (hθ : 1 ≤ θ) (hδ : 0 < δ) : (Verification.bb5 θ δ hθ hδ).extremalCoefficient = (2 - 2 ^ (-1 / δ)) ^ (1 / θ)

theorem Papers.AnsariRockel2024.bb5_tails (θ δ : ℝ) (hθ : 1 ≤ θ) (hδ : 0 < δ) : (Verification.bb5 θ δ hθ hδ).HasLowerTailDependence 0 ∧ (Verification.bb5 θ δ hθ hδ).HasUpperTailDependence (2 - (2 - 2 ^ (-1 / δ)) ^ (1 / θ))