← Copula mathematical handbook

Nelsen 8 dependence exclusions

A positive diagonal point has CDF zero. This excludes PQD, CI, CDF-level TP2, and an MTP2 density for every finite θ ≥ 1. The θ = 1 endpoint is CD.

theorem ProbabilityTheory.Copula.not_isPQD_nelsen8 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen8 θ hθ).IsPQD

Every Nelsen 8 copula fails positive quadrant dependence.

theorem ProbabilityTheory.Copula.not_isCI_nelsen8 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen8 θ hθ).IsCI

No Nelsen 8 copula is conditionally increasing.

theorem ProbabilityTheory.Copula.not_isTP2CDF_nelsen8 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen8 θ hθ).IsTP2CDF

Nelsen 8 never has a TP2 CDF.

theorem ProbabilityTheory.Copula.not_hasMTP2Density_nelsen8 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen8 θ hθ).HasMTP2Density

Nelsen 8 never has an MTP2 Lebesgue density.

theorem ProbabilityTheory.Copula.isCD_nelsen8_one : (nelsen8 1 ⋯).IsCD

The lower-Fréchet endpoint of Nelsen 8 is conditionally decreasing.

theorem ProbabilityTheory.Copula.not_isCD_nelsen8 (θ : ℝ) (hθ : 1 < θ) : ¬(nelsen8 θ ⋯).IsCD

Nelsen 8 is not conditionally decreasing at any parameter strictly above one.

theorem ProbabilityTheory.Copula.isCD_nelsen8_iff (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen8 θ hθ).IsCD ↔ θ = 1

The lower-Fréchet endpoint is the only conditionally decreasing Nelsen 8 copula.