Tail dependence from one-sided derivatives of the diagonal #
The diagonal may be represented by any real function agreeing on [0,1].
Only a derivative within this interval is required at the relevant endpoint.
theorem
ProbabilityTheory.Copula.hasLowerTailDependence_of_hasDerivWithinAt
{C : Copula 2}
{f : ℝ → ℝ}
{l : ℝ}
(hf : ∀ (t : ↑unitInterval), f ↑t = C.diagonal t)
(hd : HasDerivWithinAt f l (Set.Icc 0 1) 0)
:
The right derivative of the diagonal at zero is the lower tail coefficient.
theorem
ProbabilityTheory.Copula.hasUpperTailDependence_of_hasDerivWithinAt
{C : Copula 2}
{f : ℝ → ℝ}
{l : ℝ}
(hf : ∀ (t : ↑unitInterval), f ↑t = C.diagonal t)
(hd : HasDerivWithinAt f l (Set.Icc 0 1) 1)
:
C.HasUpperTailDependence (2 - l)
Two minus the left derivative at one is the upper tail coefficient.