← Copula mathematical handbook

Quadrant dependence of Nelsen's families 7, 9, 10, 11, 13

• #7: NQD for all θ ∈ [0, 1]; PQD iff θ = 1 (independence);
• #9, #10, #11: NQD, and not PQD (for #11 because the generator is non-strict);
• #13: PQD iff θ ≥ 1, NQD iff θ ≤ 1; for θ < 1 (resp. θ > 1) the sign of dependence is witnessed by strict convexity (resp. concavity) of x ↦ x^{1/θ}.

Family 13

theorem ProbabilityTheory.Copula.not_isPQD_nelsen13 (θ : ℝ) (hθ : 0 < θ) (h1 : θ < 1) : ¬(nelsen13 θ hθ).IsPQD

Nelsen's family 13 is not PQD for 0 < θ < 1.

theorem ProbabilityTheory.Copula.not_isNQD_nelsen13 (θ : ℝ) (h1 : 1 < θ) : ¬(nelsen13 θ ⋯).IsNQD

Nelsen's family 13 is not NQD for θ > 1.

theorem ProbabilityTheory.Copula.isPQD_nelsen13_iff (θ : ℝ) (hθ : 0 < θ) : (nelsen13 θ hθ).IsPQD ↔ 1 ≤ θ

Nelsen's family 13 is PQD iff θ ≥ 1.

theorem ProbabilityTheory.Copula.isNQD_nelsen13_iff (θ : ℝ) (hθ : 0 < θ) : (nelsen13 θ hθ).IsNQD ↔ θ ≤ 1

Nelsen's family 13 is NQD iff θ ≤ 1.

Families 9 and 10

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

Nelsen's family 9 (Gumbel–Barnett) is not PQD.

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

Nelsen's family 10 is not PQD.

Family 11

theorem ProbabilityTheory.Copula.isNQD_nelsen11 (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) : (nelsen11 θ hθ h2).IsNQD

Nelsen's family 11 is NQD.

theorem ProbabilityTheory.Copula.not_isPQD_nelsen11 (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) : ¬(nelsen11 θ hθ h2).IsPQD

Nelsen's family 11 is not PQD (its generator is non-strict).

Family 7

theorem ProbabilityTheory.Copula.isNQD_nelsen7 (θ : ↑unitInterval) : (nelsen7 θ).IsNQD

Nelsen's family 7 is NQD for every θ ∈ [0, 1].

theorem ProbabilityTheory.Copula.not_isPQD_nelsen7 (θ : ↑unitInterval) (hθ : θ ≠ 1) : ¬(nelsen7 θ).IsPQD

Nelsen's family 7 is not PQD for θ < 1.

theorem ProbabilityTheory.Copula.isPQD_nelsen7_iff (θ : ↑unitInterval) : (nelsen7 θ).IsPQD ↔ θ = 1

Nelsen's family 7 is PQD iff θ = 1.