theorem
Papers.AnsariRockel2024.huslerReiss_extremalCoefficient
(δ : ℝ)
(hδ : 0 < δ)
:
(Verification.huslerReissPositive δ hδ).extremalCoefficient = 2 * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (1 / δ)
theorem
Papers.AnsariRockel2024.huslerReiss_tails
(δ : ℝ)
(hδ : 0 < δ)
:
(Verification.huslerReissPositive δ hδ).HasLowerTailDependence 0 ∧ (Verification.huslerReissPositive δ hδ).HasUpperTailDependence
(2 - 2 * ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (1 / δ))