← Copula mathematical handbook

Quadrant dependence of families of Nelsen's Table 4.1 via generators

Applications of the generator criteria of Copula.Archimedean.Concordance (Nelsen, An Introduction to Copulas, second edition, Theorem 4.4.2 with Π as one of the copulas): a strict Archimedean copula is PQD iff ψ(x) ψ(y) ≤ ψ(x + y), and an Archimedean copula is NQD iff φ(uv) ≤ φ(u) + φ(v) on (0, 1].

• family 4.2.9 (0 < θ ≤ 1) is NQD (isNQD_nelsen9): 1 + θ(A + B) ≤ (1 + θA)(1 + θB);
• family 4.2.10 (0 < θ ≤ 1) is NQD (isNQD_nelsen10): 2ab − 1 ≤ (2a − 1)(2b − 1) for a, b ≥ 1;
• family 4.2.13 is PQD for θ ≥ 1 (isPQD_nelsen13) and NQD for 0 < θ ≤ 1 (isNQD_nelsen13), by concavity resp. convexity of t ↦ t^p on [1, ∞) (one_add_add_rpow_add_one_le, one_add_rpow_add_one_le_of_one_le);
• families 4.2.19 and 4.2.20 (θ > 0) are PQD (isPQD_nelsen19, isPQD_nelsen20), from log(e^a + e^b − 1) ≤ a + b for a, b ≥ 0.

theorem ProbabilityTheory.Copula.one_add_add_rpow_add_one_le {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : (1 + (a + b)) ^ p + 1 ≤ (1 + a) ^ p + (1 + b) ^ p

(1 + a + b)^p + 1 ≤ (1 + a)^p + (1 + b)^p for 0 ≤ p ≤ 1 and a, b ≥ 0.

theorem ProbabilityTheory.Copula.one_add_rpow_add_one_le_of_one_le {p : ℝ} (hp : 1 ≤ p) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : (1 + a) ^ p + (1 + b) ^ p ≤ (1 + (a + b)) ^ p + 1

(1 + a)^p + (1 + b)^p ≤ (1 + a + b)^p + 1 for p ≥ 1 and a, b ≥ 0.

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

Nelsen's family 9 is negatively quadrant dependent.

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

Nelsen's family 10 is negatively quadrant dependent.

theorem ProbabilityTheory.Copula.isPQD_nelsen13 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen13 θ ⋯).IsPQD

Nelsen's family 13 is positively quadrant dependent for θ ≥ 1.

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

Nelsen's family 13 is negatively quadrant dependent for 0 < θ ≤ 1.

theorem ProbabilityTheory.Copula.isPQD_nelsen19 (θ : ℝ) (hθ : 0 < θ) : (nelsen19 θ hθ).IsPQD

Nelsen's family 19 is positively quadrant dependent.

theorem ProbabilityTheory.Copula.isPQD_nelsen20 (θ : ℝ) (hθ : 0 < θ) : (nelsen20 θ hθ).IsPQD

Nelsen's family 20 is positively quadrant dependent.