← Mathematical handbook

Extreme-value copulas and closure under power products

The defining identity is max-stability: C(u₁^t,...,u_d^t) = C(u)^t for every positive real t. All coordinates of the closed cube are included.

def ProbabilityTheory.Copula.IsExtremeValue {d : ℕ} (C : Copula d) : Prop

The max-stability characterization of an extreme-value copula.

Equations

• C.IsExtremeValue = ∀ (u : Fin d → ↑unitInterval) (t : ℝ) (ht : 0 < t), (C.cdf fun (i : Fin d) => ProbabilityTheory.Copula.unitPower (u i) t ⋯) = C.cdf u ^ t

theorem ProbabilityTheory.Copula.isExtremeValue_independence (d : ℕ) : (independence d).IsExtremeValue

theorem ProbabilityTheory.Copula.isExtremeValue_comonotonic (d : ℕ) : (comonotonic d).IsExtremeValue

theorem ProbabilityTheory.Copula.IsExtremeValue.maxProduct {d : ℕ} {C D : Copula d} (hC : C.IsExtremeValue) (hD : D.IsExtremeValue) (a : Fin d → ↑unitInterval) : (C.maxProduct D a).IsExtremeValue