← Copula mathematical handbook

Exact Genest–Ghoudi dependence exclusions and CD range

theorem ProbabilityTheory.Copula.not_isPQD_genestGhoudi (θ : ℝ) (hθ : 1 ≤ θ) : ¬(genestGhoudi θ hθ).IsPQD

Every Genest–Ghoudi copula fails positive quadrant dependence.

theorem ProbabilityTheory.Copula.not_isCI_genestGhoudi (θ : ℝ) (hθ : 1 ≤ θ) : ¬(genestGhoudi θ hθ).IsCI

No Genest–Ghoudi copula is conditionally increasing.

theorem ProbabilityTheory.Copula.not_isTP2CDF_genestGhoudi (θ : ℝ) (hθ : 1 ≤ θ) : ¬(genestGhoudi θ hθ).IsTP2CDF

No Genest–Ghoudi CDF is TP2.

theorem ProbabilityTheory.Copula.not_hasMTP2Density_genestGhoudi (θ : ℝ) (hθ : 1 ≤ θ) : ¬(genestGhoudi θ hθ).HasMTP2Density

No Genest–Ghoudi copula has an MTP2 Lebesgue density.

theorem ProbabilityTheory.Copula.not_isCD_genestGhoudi (θ : ℝ) (hθ : 1 < θ) : ¬(genestGhoudi θ ⋯).IsCD

Positive upper-tail dependence excludes CD for θ>1.

theorem ProbabilityTheory.Copula.isCD_genestGhoudi_one : (genestGhoudi 1 ⋯).IsCD

The countermonotonic endpoint is CD.

theorem ProbabilityTheory.Copula.isCD_genestGhoudi_iff (θ : ℝ) (hθ : 1 ≤ θ) : (genestGhoudi θ hθ).IsCD ↔ θ = 1

Genest–Ghoudi is CD exactly at θ=1.