← Mathematical handbook

Explicit extreme-value tail coefficients

Power diagonals give the extremal coefficient and tail limits for Marshall–Olkin, Cuadras–Augé, Gumbel–Hougaard and Tawn. Singular parameter endpoints are included; in particular the lower tail of M is one.

theorem ProbabilityTheory.Copula.hasPowerDiagonal_marshallOlkin (α β : ↑unitInterval) : (marshallOlkin α β).HasPowerDiagonal (2 - min ↑α ↑β)

theorem ProbabilityTheory.Copula.extremalCoefficient_marshallOlkin (α β : ↑unitInterval) : (marshallOlkin α β).extremalCoefficient = 2 - min ↑α ↑β

theorem ProbabilityTheory.Copula.hasUpperTailDependence_marshallOlkin (α β : ↑unitInterval) : (marshallOlkin α β).HasUpperTailDependence (min ↑α ↑β)

theorem ProbabilityTheory.Copula.hasLowerTailDependence_marshallOlkin (α β : ↑unitInterval) : (marshallOlkin α β).HasLowerTailDependence (if α = 1 ∧ β = 1 then 1 else 0)

theorem ProbabilityTheory.Copula.hasPowerDiagonal_cuadrasAuge (α : ↑unitInterval) : (cuadrasAuge α).HasPowerDiagonal (2 - ↑α)

theorem ProbabilityTheory.Copula.extremalCoefficient_cuadrasAuge (α : ↑unitInterval) : (cuadrasAuge α).extremalCoefficient = 2 - ↑α

theorem ProbabilityTheory.Copula.hasUpperTailDependence_cuadrasAuge (α : ↑unitInterval) : (cuadrasAuge α).HasUpperTailDependence ↑α

theorem ProbabilityTheory.Copula.hasLowerTailDependence_cuadrasAuge (α : ↑unitInterval) : (cuadrasAuge α).HasLowerTailDependence (if α = 1 then 1 else 0)

theorem ProbabilityTheory.Copula.hasPowerDiagonal_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).HasPowerDiagonal (2 ^ θ⁻¹)

theorem ProbabilityTheory.Copula.extremalCoefficient_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).extremalCoefficient = 2 ^ θ⁻¹

theorem ProbabilityTheory.Copula.hasUpperTailDependence_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)

theorem ProbabilityTheory.Copula.hasLowerTailDependence_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).HasLowerTailDependence 0

theorem ProbabilityTheory.Copula.hasPowerDiagonal_tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : (tawn θ hθ α β).HasPowerDiagonal (2 - ↑α - ↑β + (↑α ^ θ + ↑β ^ θ) ^ θ⁻¹)

theorem ProbabilityTheory.Copula.extremalCoefficient_tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : (tawn θ hθ α β).extremalCoefficient = 2 - ↑α - ↑β + (↑α ^ θ + ↑β ^ θ) ^ θ⁻¹

theorem ProbabilityTheory.Copula.hasUpperTailDependence_tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : (tawn θ hθ α β).HasUpperTailDependence (↑α + ↑β - (↑α ^ θ + ↑β ^ θ) ^ θ⁻¹)

theorem ProbabilityTheory.Copula.hasLowerTailDependence_tawn (θ : ℝ) (hθ : 1 ≤ θ) (α β : ↑unitInterval) : (tawn θ hθ α β).HasLowerTailDependence 0