Exact lower and upper tail dependence of the signed Clayton family #
theorem
ProbabilityTheory.Copula.hasLowerTailDependence_clayton_positive
(θ : ℝ)
(hθ : 0 < θ)
:
(clayton 2 θ hθ).HasLowerTailDependence (2 ^ (-1 / θ))
The lower-tail coefficient of positive Clayton is 2 ^ (-1 / θ).
theorem
ProbabilityTheory.Copula.hasLowerTailDependence_clayton_negative
(θ : ℝ)
(hθ : -1 ≤ θ)
(hn : θ < 0)
:
(claytonNegative θ hθ hn).HasLowerTailDependence 0
Every admissible negative Clayton copula has zero lower-tail dependence.
theorem
ProbabilityTheory.Copula.hasUpperTailDependence_clayton_negative
(θ : ℝ)
(hθ : -1 ≤ θ)
(hn : θ < 0)
:
(claytonNegative θ hθ hn).HasUpperTailDependence 0
Every admissible negative Clayton copula has zero upper-tail dependence.
theorem
ProbabilityTheory.Copula.hasUpperTailDependence_clayton_positive
(θ : ℝ)
(hθ : 0 < θ)
:
(clayton 2 θ hθ).HasUpperTailDependence 0
Positive Clayton has no upper-tail dependence.