Tail independence of the Plackett family #
The diagonal δ(t) = C_θ(t,t) of a Plackett copula has derivative 0 at t = 0 (the
discriminant equals 1 there), so λ_L = 0; radial symmetry then gives λ_U = 0
(Nelsen 2006, §5.4: the Plackett copulas are tail independent for every θ > 0).
theorem
ProbabilityTheory.Copula.hasDerivAt_plackettCDF_diagonal_zero
(θ : ℝ)
:
HasDerivAt (fun (t : ℝ) => plackettCDF θ t t) 0 0
theorem
ProbabilityTheory.Copula.hasLowerTailDependence_plackett
(θ : ℝ)
(hθ : 0 < θ)
:
(plackett θ hθ).HasLowerTailDependence 0
The Plackett copulas have no lower tail dependence.
theorem
ProbabilityTheory.Copula.hasUpperTailDependence_plackett
(θ : ℝ)
(hθ : 0 < θ)
:
(plackett θ hθ).HasUpperTailDependence 0
The Plackett copulas have no upper tail dependence.