theorem
Papers.AnsariRockel2024.bb5_isExtremeValue
(θ δ : ℝ)
(hθ : 1 ≤ θ)
(hδ : 0 < δ)
:
(Verification.bb5 θ δ hθ hδ).IsExtremeValue
theorem
Papers.AnsariRockel2024.bb5_isCI
(θ δ : ℝ)
(hθ : 1 ≤ θ)
(hδ : 0 < δ)
:
(Verification.bb5 θ δ hθ hδ).IsCI
theorem
Papers.AnsariRockel2024.bb5_pickands_interior
(θ δ : ℝ)
(hθ : 1 ≤ θ)
(hδ : 0 < δ)
(t : ↑unitInterval)
(ht : ↑t ∈ Set.Ioo 0 1)
:
Verification.copulaPickands (Verification.bb5 θ δ hθ hδ) t = Verification.bb5TailKernel θ δ (1 - ↑t) ↑t