Documentation

Copula.Diagonal.Power

← Mathematical handbook

Power diagonal sections #

The power-diagonal property does not assume max-stability. Its exponent lies in [1,2], determines both tail coefficients, and equals one exactly for M.

def ProbabilityTheory.Copula.HasPowerDiagonal (C : Copula 2) (κ : ℝ) :

A copula with diagonal section δ(t) = t^κ, including the endpoints.

Equations

C.HasPowerDiagonal κ = ∀ (t : ↑unitInterval), C.diagonal t = ↑t ^ κ

Instances For

theorem ProbabilityTheory.Copula.HasPowerDiagonal.one_le {C : Copula 2} {κ : ℝ} (h : C.HasPowerDiagonal κ) :

1 ≤ κ

theorem ProbabilityTheory.Copula.HasPowerDiagonal.hasUpperTailDependence {C : Copula 2} {κ : ℝ} (h : C.HasPowerDiagonal κ) :

C.HasUpperTailDependence (2 - κ)

theorem ProbabilityTheory.Copula.HasPowerDiagonal.mem_Icc {C : Copula 2} {κ : ℝ} (h : C.HasPowerDiagonal κ) :

κ ∈ Set.Icc 1 2

theorem ProbabilityTheory.Copula.HasPowerDiagonal.hasLowerTailDependence_zero {C : Copula 2} {κ : ℝ} (h : C.HasPowerDiagonal κ) (hκ : 1 < κ) :

C.HasLowerTailDependence 0

theorem ProbabilityTheory.Copula.hasPowerDiagonal_one_iff (C : Copula 2) :

C.HasPowerDiagonal 1 ↔ C = comonotonic 2

theorem ProbabilityTheory.Copula.HasPowerDiagonal.hasLowerTailDependence {C : Copula 2} {κ : ℝ} (h : C.HasPowerDiagonal κ) :

C.HasLowerTailDependence (if κ = 1 then 1 else 0)

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

a = b