Nelsen 14 tail coefficients from Table 3 #
theorem
Papers.AnsariRockel2024.nelsen14_tails
(θ : ℝ)
(hθ : 1 ≤ θ)
:
(ProbabilityTheory.Copula.nelsen14 θ hθ).HasLowerTailDependence (1 / 2) ∧ (ProbabilityTheory.Copula.nelsen14 θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)
Both printed Nelsen 14 tail coefficients for every finite admissible parameter.