Exact lower and upper tail dependence of Nelsen 14 #
theorem
ProbabilityTheory.Copula.hasLowerTailDependence_nelsen14
(θ : ℝ)
(hθ : 1 ≤ θ)
:
(nelsen14 θ hθ).HasLowerTailDependence (1 / 2)
Nelsen 14 has lower-tail coefficient one half for every finite parameter.
theorem
ProbabilityTheory.Copula.hasUpperTailDependence_nelsen14
(θ : ℝ)
(hθ : 1 ≤ θ)
:
(nelsen14 θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)
Nelsen 14 has upper-tail coefficient 2−2^(1/θ) for every finite parameter.