← Copula mathematical handbook

Quadrant dependence of Nelsen's families 8, 18, 21, 22

• #8: NQD iff θ ≤ 2 (for θ > 2 the copula is neither PQD nor NQD: the printed CDF exceeds u v at u = v = θ / (2 (θ - 1)));
• #18, #21: never PQD (non-strict generators); #18 never NQD (λ_U = 1), #21 NQD iff θ = 1;
• #22: NQD for all θ ∈ (0, 1] (inner power of the θ = 1 member) and never PQD.

Family 8

theorem ProbabilityTheory.Copula.isNQD_nelsen8 (θ : ℝ) (hθ : 1 ≤ θ) (h2 : θ ≤ 2) : (nelsen8 θ hθ).IsNQD

Nelsen's family 8 is NQD for 1 ≤ θ ≤ 2.

theorem ProbabilityTheory.Copula.not_isNQD_nelsen8 (θ : ℝ) (hθ : 2 < θ) : ¬(nelsen8 θ ⋯).IsNQD

Nelsen's family 8 is not NQD for θ > 2.

theorem ProbabilityTheory.Copula.isNQD_nelsen8_iff (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen8 θ hθ).IsNQD ↔ θ ≤ 2

Nelsen's family 8 is NQD iff θ ≤ 2.

Families 18 and 21 (non-strict generators)

theorem ProbabilityTheory.Copula.not_isPQD_nelsen18 (θ : ℝ) (hθ : 2 ≤ θ) : ¬(nelsen18 θ hθ).IsPQD

Nelsen's family 18 is never PQD.

theorem ProbabilityTheory.Copula.not_isPQD_nelsen21 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen21 θ hθ).IsPQD

Nelsen's family 21 is never PQD.

Family 22

theorem ProbabilityTheory.Copula.isNQD_nelsen22 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen22 θ hθ h1).IsNQD

Nelsen's family 22 is NQD for every θ ∈ (0, 1].

theorem ProbabilityTheory.Copula.not_isPQD_nelsen22 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : ¬(nelsen22 θ hθ h1).IsPQD

Nelsen's family 22 is never PQD.