Exact Nelsen 2 tail dependence #
Both tail limits hold for every finite parameter θ ≥ 1, including the countermonotonic endpoint θ = 1.
theorem
ProbabilityTheory.Copula.hasUpperTailDependence_nelsen2
(θ : ℝ)
(hθ : 1 ≤ θ)
:
(nelsen2 θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)
The Nelsen 2 upper-tail coefficient, including the countermonotonic endpoint.
theorem
ProbabilityTheory.Copula.hasLowerTailDependence_nelsen2
(θ : ℝ)
(hθ : 1 ≤ θ)
:
(nelsen2 θ hθ).HasLowerTailDependence 0
The Nelsen 2 lower-tail coefficient vanishes for every admissible parameter.