← Copula mathematical handbook

Tail dependence of ordinal sums

A positive lower block determines lower-tail dependence, and a positive upper block determines upper-tail dependence. The equivalences include existence of the limits; no differentiability or density is assumed.

theorem ProbabilityTheory.Copula.lowerTailRatio_ordinalSum (C D : Copula 2) (a t : ↑unitInterval) (ha : 0 < a) (ht : 0 < t) (hta : t ≤ a) : (C.ordinalSum D a).lowerTailRatio t = C.lowerTailRatio (OrdinalSum.lowerCoord a t)

theorem ProbabilityTheory.Copula.upperTailRatio_ordinalSum (C D : Copula 2) (a t : ↑unitInterval) (ha : a < 1) (ht : 0 < t) (hta : t ≤ unitInterval.symm a) : (C.ordinalSum D a).upperTailRatio t = D.upperTailRatio (OrdinalSum.lowerCoord (unitInterval.symm a) t)

theorem ProbabilityTheory.Copula.HasLowerTailDependence.ordinalSum {C : Copula 2} {l : ℝ} (h : C.HasLowerTailDependence l) (D : Copula 2) (a : ↑unitInterval) (ha : 0 < a) : (C.ordinalSum D a).HasLowerTailDependence l

theorem ProbabilityTheory.Copula.HasUpperTailDependence.ordinalSum {D : Copula 2} {l : ℝ} (h : D.HasUpperTailDependence l) (C : Copula 2) (a : ↑unitInterval) (ha : a < 1) : (C.ordinalSum D a).HasUpperTailDependence l

theorem ProbabilityTheory.Copula.hasLowerTailDependence_ordinalSum_iff (C D : Copula 2) (a : ↑unitInterval) (ha : 0 < a) (l : ℝ) : (C.ordinalSum D a).HasLowerTailDependence l ↔ C.HasLowerTailDependence l

theorem ProbabilityTheory.Copula.hasUpperTailDependence_ordinalSum_iff (C D : Copula 2) (a : ↑unitInterval) (ha : a < 1) (l : ℝ) : (C.ordinalSum D a).HasUpperTailDependence l ↔ D.HasUpperTailDependence l