← Mathematical handbook

Lower and upper tail dependence

Both limits are parametrized by a tail probability t → 0+. Thus the upper threshold is 1-t. Existence is an explicit predicate, never assumed. See Nelsen, second edition, §5.4.

noncomputable def ProbabilityTheory.Copula.lowerTailRatio (C : Copula 2) (t : ↑unitInterval) : ℝ

Lower tail conditional probability at a positive tail width.

Equations

• C.lowerTailRatio t = C.diagonal t / ↑t

noncomputable def ProbabilityTheory.Copula.upperTailRatio (C : Copula 2) (t : ↑unitInterval) : ℝ

Upper tail conditional probability at threshold 1-t.

Equations

• C.upperTailRatio t = C.survivalCopula.lowerTailRatio t

def ProbabilityTheory.Copula.HasLowerTailDependence (C : Copula 2) (l : ℝ) : Prop

Existence and value of the lower tail-dependence limit.

Equations

• C.HasLowerTailDependence l = Filter.Tendsto C.lowerTailRatio (nhdsWithin 0 (Set.Ioi 0)) (nhds l)

def ProbabilityTheory.Copula.HasUpperTailDependence (C : Copula 2) (l : ℝ) : Prop

Existence and value of the upper tail-dependence limit.

Equations

• C.HasUpperTailDependence l = Filter.Tendsto C.upperTailRatio (nhdsWithin 0 (Set.Ioi 0)) (nhds l)

theorem ProbabilityTheory.Copula.tailFilter_neBot : (nhdsWithin 0 (Set.Ioi 0)).NeBot

theorem ProbabilityTheory.Copula.lowerTailRatio_mem_Icc (C : Copula 2) (t : ↑unitInterval) : C.lowerTailRatio t ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.upperTailRatio_mem_Icc (C : Copula 2) (t : ↑unitInterval) : C.upperTailRatio t ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.upperTailRatio_eq (C : Copula 2) (t : ↑unitInterval) : C.upperTailRatio t = (2 * ↑t - 1 + C.diagonal (unitInterval.symm t)) / ↑t

theorem ProbabilityTheory.Copula.upperTailRatio_eq_survival (C : Copula 2) (t : ↑unitInterval) : C.upperTailRatio t = C.survival ![unitInterval.symm t, unitInterval.symm t] / ↑t

theorem ProbabilityTheory.Copula.hasUpperTailDependence_iff_tendsto_one (C : Copula 2) (l : ℝ) : C.HasUpperTailDependence l ↔ Filter.Tendsto (fun (t : ↑unitInterval) => (1 - 2 * ↑t + C.diagonal t) / (1 - ↑t)) (nhdsWithin 1 (Set.Iio 1)) (nhds l)

Equivalence with the usual formula parametrized by a threshold tending to one.

theorem ProbabilityTheory.Copula.HasLowerTailDependence.mem_Icc {C : Copula 2} {l : ℝ} (h : C.HasLowerTailDependence l) : l ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.HasUpperTailDependence.mem_Icc {C : Copula 2} {l : ℝ} (h : C.HasUpperTailDependence l) : l ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.HasLowerTailDependence.unique {C : Copula 2} {a b : ℝ} (ha : C.HasLowerTailDependence a) (hb : C.HasLowerTailDependence b) : a = b

theorem ProbabilityTheory.Copula.HasUpperTailDependence.unique {C : Copula 2} {a b : ℝ} (ha : C.HasUpperTailDependence a) (hb : C.HasUpperTailDependence b) : a = b

theorem ProbabilityTheory.Copula.hasUpperTailDependence_iff_survivalCopula (C : Copula 2) (l : ℝ) : C.HasUpperTailDependence l ↔ C.survivalCopula.HasLowerTailDependence l

theorem ProbabilityTheory.Copula.hasLowerTailDependence_iff_survivalCopula (C : Copula 2) (l : ℝ) : C.HasLowerTailDependence l ↔ C.survivalCopula.HasUpperTailDependence l

theorem ProbabilityTheory.Copula.hasLowerTailDependence_transpose_iff (C : Copula 2) (l : ℝ) : C.transpose.HasLowerTailDependence l ↔ C.HasLowerTailDependence l

theorem ProbabilityTheory.Copula.hasUpperTailDependence_transpose_iff (C : Copula 2) (l : ℝ) : C.transpose.HasUpperTailDependence l ↔ C.HasUpperTailDependence l

theorem ProbabilityTheory.Copula.IsRadiallySymmetric.hasUpperTailDependence_iff {C : Copula 2} (h : C.IsRadiallySymmetric) (l : ℝ) : C.HasUpperTailDependence l ↔ C.HasLowerTailDependence l

theorem ProbabilityTheory.Copula.LowerOrthantLE.lowerTailDependence_le {C D : Copula 2} (h : C.LowerOrthantLE D) {a b : ℝ} (ha : C.HasLowerTailDependence a) (hb : D.HasLowerTailDependence b) : a ≤ b

theorem ProbabilityTheory.Copula.LowerOrthantLE.upperTailDependence_le {C D : Copula 2} (h : C.LowerOrthantLE D) {a b : ℝ} (ha : C.HasUpperTailDependence a) (hb : D.HasUpperTailDependence b) : a ≤ b

theorem ProbabilityTheory.Copula.HasLowerTailDependence.mix {C D : Copula 2} {a b : ℝ} (hC : C.HasLowerTailDependence a) (hD : D.HasLowerTailDependence b) (w : ↑unitInterval) : (C.mix D w).HasLowerTailDependence (↑w * a + (1 - ↑w) * b)

theorem ProbabilityTheory.Copula.HasUpperTailDependence.mix {C D : Copula 2} {a b : ℝ} (hC : C.HasUpperTailDependence a) (hD : D.HasUpperTailDependence b) (w : ↑unitInterval) : (C.mix D w).HasUpperTailDependence (↑w * a + (1 - ↑w) * b)