Nelsen 12 tail coefficients from Table 3 #
theorem
Papers.AnsariRockel2024.nelsen12_tails
(θ : ℝ)
(hθ : 1 ≤ θ)
:
(ProbabilityTheory.Copula.nelsen12 θ hθ).HasLowerTailDependence (2 ^ θ⁻¹)⁻¹ ∧ (ProbabilityTheory.Copula.nelsen12 θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)
Both printed Nelsen 12 tail coefficients for every finite admissible parameter.
The lower expression is algebraically equal to 2 ^ (-1 / θ).