theorem
ProbabilityTheory.Copula.hasLowerTailDependence_nelsen12
(θ : ℝ)
(hθ : 1 ≤ θ)
:
(nelsen12 θ hθ).HasLowerTailDependence (2 ^ θ⁻¹)⁻¹
The Nelsen 12 lower-tail coefficient for every finite parameter.
theorem
ProbabilityTheory.Copula.hasUpperTailDependence_nelsen12
(θ : ℝ)
(hθ : 1 ≤ θ)
:
(nelsen12 θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)
The Nelsen 12 upper-tail coefficient for every finite parameter.