← Copula mathematical handbook

Quadrant dependence of families with tail dependence

Nonzero tail coefficients exclude NQD (isNQD_hasLowerTailDependence_zero). This gives, for Nelsen's Table 4.1 and Gumbel's family:

• Gumbel (#4): PQD for all θ ≥ 1 (from the TP2 property); NQD iff θ = 1;
• #2 and #15: NQD iff θ = 1 (the lower Fréchet bound W);
• #12, #14, #19, #20: not NQD (they are PQD by earlier results);
• #16 (θ > 0): not NQD; #18: not NQD; #21: NQD iff θ = 1.

theorem ProbabilityTheory.Copula.isPQD_gumbel (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).IsPQD

Gumbel's copula is PQD for all θ ≥ 1.

theorem ProbabilityTheory.Copula.not_isNQD_gumbel (θ : ℝ) (hθ : 1 < θ) : ¬(gumbel θ ⋯).IsNQD

Gumbel's copula is not NQD for θ > 1.

theorem ProbabilityTheory.Copula.isNQD_gumbel_iff (θ : ℝ) (hθ : 1 ≤ θ) : (gumbel θ hθ).IsNQD ↔ θ = 1

Gumbel's copula is NQD iff θ = 1 (independence).

theorem ProbabilityTheory.Copula.not_isNQD_nelsen2 (θ : ℝ) (hθ : 1 < θ) : ¬(nelsen2 θ ⋯).IsNQD

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

theorem ProbabilityTheory.Copula.isNQD_nelsen2_iff (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen2 θ hθ).IsNQD ↔ θ = 1

Nelsen's family 2 is NQD iff θ = 1 (the lower Fréchet bound).

theorem ProbabilityTheory.Copula.not_isNQD_genestGhoudi (θ : ℝ) (hθ : 1 < θ) : ¬(genestGhoudi θ ⋯).IsNQD

Nelsen's family 15 (Genest–Ghoudi) is not NQD for θ > 1.

theorem ProbabilityTheory.Copula.isNQD_genestGhoudi_iff (θ : ℝ) (hθ : 1 ≤ θ) : (genestGhoudi θ hθ).IsNQD ↔ θ = 1

Nelsen's family 15 is NQD iff θ = 1 (the lower Fréchet bound).

theorem ProbabilityTheory.Copula.not_isNQD_nelsen12 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen12 θ hθ).IsNQD

Nelsen's family 12 is never NQD (λ_L = 2^{-1/θ} > 0).

theorem ProbabilityTheory.Copula.not_isNQD_nelsen14 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(nelsen14 θ hθ).IsNQD

Nelsen's family 14 is never NQD (λ_L = 1/2).

theorem ProbabilityTheory.Copula.not_isNQD_nelsen16 (θ : ℝ) (hθ : 0 < θ) : ¬(nelsen16 θ ⋯).IsNQD

Nelsen's family 16 is not NQD for θ > 0 (λ_L = 1/2).

theorem ProbabilityTheory.Copula.not_isNQD_nelsen18 (θ : ℝ) (hθ : 2 ≤ θ) : ¬(nelsen18 θ hθ).IsNQD

Nelsen's family 18 is never NQD (λ_U = 1).

theorem ProbabilityTheory.Copula.not_isNQD_nelsen19 (θ : ℝ) (hθ : 0 < θ) : ¬(nelsen19 θ hθ).IsNQD

Nelsen's family 19 is never NQD (λ_L = 1).

theorem ProbabilityTheory.Copula.not_isNQD_nelsen20 (θ : ℝ) (hθ : 0 < θ) : ¬(nelsen20 θ hθ).IsNQD

Nelsen's family 20 is never NQD (λ_L = 1).

theorem ProbabilityTheory.Copula.not_isNQD_nelsen21 (θ : ℝ) (hθ : 1 < θ) : ¬(nelsen21 θ ⋯).IsNQD

Nelsen's family 21 is not NQD for θ > 1 (λ_U = 2 - 2^{1/θ}).

theorem ProbabilityTheory.Copula.isNQD_nelsen21_iff (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen21 θ hθ).IsNQD ↔ θ = 1

Nelsen's family 21 is NQD iff θ = 1 (the lower Fréchet bound).