← Copula mathematical handbook

Quadrant dependence of Nelsen's family 17

The inverse generator of family 17 is ψ(s) = (1 + d e^{-s})^q - 1 with q = -1/θ and d = 2^{-θ} - 1, so that q d > 0. With E = e^{-s} and B = 1 + d E one finds ψ ψ'' - ψ'² = q d E B^{q-2} (B^q - 1 - q (B - 1)). By Bernoulli's inequality the bracket is strictly positive for q < 0 and q > 1, and strictly negative for 0 < q < 1. Hence:

• θ > 0 (q < 0) and -1 < θ < 0 (q > 1): PQD and not NQD;
• θ < -1 (0 < q < 1): NQD and not PQD;
• θ = -1: independence.

theorem ProbabilityTheory.Copula.N17Quadrant.psi_pos {d q : ℝ} (hd : -1 < d) (hd0 : d ≠ 0) (hqd : 0 < q * d) {t : ℝ} (ht : 0 ≤ t) : 0 < (1 + d * Real.exp (-t)) ^ q - 1

Positivity of the inverse generator.

theorem ProbabilityTheory.Copula.N17Quadrant.strictConvexOn_log {d q : ℝ} (hd : -1 < d) (hd0 : d ≠ 0) (hqd : 0 < q * d) (hq : q < 0 ∨ 1 < q) : StrictConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log ((1 + d * Real.exp (-t)) ^ q - 1)

Strict log-convexity when q < 0 or q > 1.

theorem ProbabilityTheory.Copula.N17Quadrant.strictConcaveOn_log {d q : ℝ} (hd : -1 < d) (hd0 : d ≠ 0) (hqd : 0 < q * d) (hq0 : 0 < q) (hq1 : q < 1) : StrictConcaveOn ℝ (Set.Ici 0) fun (t : ℝ) => Real.log ((1 + d * Real.exp (-t)) ^ q - 1)

Strict log-concavity when 0 < q < 1.

theorem ProbabilityTheory.Copula.N17Quadrant.params (θ : ℝ) (hθ : θ ≠ 0) : -1 < 2 ^ (-θ) - 1 ∧ 2 ^ (-θ) - 1 ≠ 0 ∧ 0 < -θ⁻¹ * (2 ^ (-θ) - 1)

The constants d = 2^{-θ} - 1 and q = -1/θ satisfy -1 < d, d ≠ 0 and 0 < q d.

theorem ProbabilityTheory.Copula.isPQD_and_not_isNQD_nelsen17 (θ : ℝ) (hθ : θ ≠ 0) (h : -1 < θ) : (nelsen17 θ hθ).IsPQD ∧ ¬(nelsen17 θ hθ).IsNQD

Nelsen's family 17 is PQD and not NQD for θ > 0 and for -1 < θ < 0.

theorem ProbabilityTheory.Copula.isNQD_and_not_isPQD_nelsen17 (θ : ℝ) (hθ : θ ≠ 0) (h : θ < -1) : (nelsen17 θ hθ).IsNQD ∧ ¬(nelsen17 θ hθ).IsPQD

Nelsen's family 17 is NQD and not PQD for θ < -1.

theorem ProbabilityTheory.Copula.isPQD_nelsen17_iff (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).IsPQD ↔ -1 ≤ θ

Nelsen's family 17 is PQD iff θ ≥ -1.

theorem ProbabilityTheory.Copula.isNQD_nelsen17_iff (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).IsNQD ↔ θ ≤ -1

Nelsen's family 17 is NQD iff θ ≤ -1.