Documentation

Copula.Dependence.ConditionalMonotonicity

← Copula mathematical handbook

Conditional increasingness and decreasingness in both directions #

The CI/CD terminology follows Ansari–Rockel, Definition 2.5. IsSI is directional CIS; IsSD is its convex-section counterpart, CDS.

def ProbabilityTheory.Copula.IsSD (C : Copula 2) :

Stochastic decreasingness of the second coordinate given the first.

Equations

C.IsSD = ∀ (a b c v : ↑unitInterval), a ≤ b → b ≤ c → (↑c - ↑a) * C.cdf ![b, v] ≤ (↑b - ↑a) * C.cdf ![c, v] + (↑c - ↑b) * C.cdf ![a, v]

Instances For

def ProbabilityTheory.Copula.IsCI (C : Copula 2) :

Conditional increasingness in both coordinate directions.

Equations

C.IsCI = (C.IsSI ∧ C.transpose.IsSI)

Instances For

def ProbabilityTheory.Copula.IsCD (C : Copula 2) :

Conditional decreasingness in both coordinate directions.

Equations

C.IsCD = (C.IsSD ∧ C.transpose.IsSD)

Instances For

theorem ProbabilityTheory.Copula.IsSD.isNQD {C : Copula 2} (h : C.IsSD) :

theorem ProbabilityTheory.Copula.IsCI.isSI {C : Copula 2} (h : C.IsCI) :

theorem ProbabilityTheory.Copula.IsCD.isSD {C : Copula 2} (h : C.IsCD) :

theorem ProbabilityTheory.Copula.IsCI.isPQD {C : Copula 2} (h : C.IsCI) :

theorem ProbabilityTheory.Copula.IsCD.isNQD {C : Copula 2} (h : C.IsCD) :

@[simp]

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

C.transpose.IsCI ↔ C.IsCI

@[simp]

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

C.transpose.IsCD ↔ C.IsCD

theorem ProbabilityTheory.Copula.IsExchangeable.isCI_iff {C : Copula 2} (h : C.IsExchangeable) :

C.IsCI ↔ C.IsSI

theorem ProbabilityTheory.Copula.IsExchangeable.isCD_iff {C : Copula 2} (h : C.IsExchangeable) :

C.IsCD ↔ C.IsSD

theorem ProbabilityTheory.Copula.IsArchimedean.isCI_iff {C : Copula 2} (h : C.IsArchimedean) :

C.IsCI ↔ C.IsSI

theorem ProbabilityTheory.Copula.IsArchimedean.isCD_iff {C : Copula 2} (h : C.IsArchimedean) :

C.IsCD ↔ C.IsSD

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

(C.reflect {1}).IsSI ↔ C.IsSD

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

(C.reflect {1}).IsSD ↔ C.IsSI

theorem ProbabilityTheory.Copula.isSD_independence :

(independence 2).IsSD

theorem ProbabilityTheory.Copula.isCI_independence :

(independence 2).IsCI

theorem ProbabilityTheory.Copula.isCD_independence :

(independence 2).IsCD

theorem ProbabilityTheory.Copula.isCI_comonotonic :

(comonotonic 2).IsCI

theorem ProbabilityTheory.Copula.isSD_countermonotonic :

countermonotonic.IsSD

theorem ProbabilityTheory.Copula.isCD_countermonotonic :

countermonotonic.IsCD

theorem ProbabilityTheory.Copula.isSD_fgm (θ : ℝ) (hθ : |θ| ≤ 1) (hneg : θ ≤ 0) :

(fgm θ hθ).IsSD

theorem ProbabilityTheory.Copula.isSD_fgm_iff (θ : ℝ) (hθ : |θ| ≤ 1) :

(fgm θ hθ).IsSD ↔ θ ≤ 0

theorem ProbabilityTheory.Copula.isCI_fgm_iff (θ : ℝ) (hθ : |θ| ≤ 1) :

(fgm θ hθ).IsCI ↔ 0 ≤ θ

theorem ProbabilityTheory.Copula.isCD_fgm_iff (θ : ℝ) (hθ : |θ| ≤ 1) :

(fgm θ hθ).IsCD ↔ θ ≤ 0