← Copula mathematical handbook

Tail-dependence benchmarks and mixture families

theorem ProbabilityTheory.Copula.hasLowerTailDependence_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).HasLowerTailDependence 0

theorem ProbabilityTheory.Copula.hasUpperTailDependence_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).HasUpperTailDependence 0

theorem ProbabilityTheory.Copula.hasLowerTailDependence_independence : (independence 2).HasLowerTailDependence 0

theorem ProbabilityTheory.Copula.hasUpperTailDependence_independence : (independence 2).HasUpperTailDependence 0

theorem ProbabilityTheory.Copula.hasLowerTailDependence_comonotonic : (comonotonic 2).HasLowerTailDependence 1

theorem ProbabilityTheory.Copula.hasUpperTailDependence_comonotonic : (comonotonic 2).HasUpperTailDependence 1

theorem ProbabilityTheory.Copula.hasLowerTailDependence_countermonotonic : countermonotonic.HasLowerTailDependence 0

theorem ProbabilityTheory.Copula.hasUpperTailDependence_countermonotonic : countermonotonic.HasUpperTailDependence 0

theorem ProbabilityTheory.Copula.hasLowerTailDependence_frechet (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).HasLowerTailDependence a

theorem ProbabilityTheory.Copula.isRadiallySymmetric_frechet (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).IsRadiallySymmetric

theorem ProbabilityTheory.Copula.hasUpperTailDependence_frechet (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (frechet a b ha hb hab).HasUpperTailDependence a

theorem ProbabilityTheory.Copula.hasLowerTailDependence_mardia (θ : ℝ) (hθ : |θ| ≤ 1) : (mardia θ hθ).HasLowerTailDependence (θ ^ 2 * (1 + θ) / 2)

theorem ProbabilityTheory.Copula.hasUpperTailDependence_mardia (θ : ℝ) (hθ : |θ| ≤ 1) : (mardia θ hθ).HasUpperTailDependence (θ ^ 2 * (1 + θ) / 2)