Documentation

Copula.Archimedean.QuadrantN16

← Copula mathematical handbook

Quadrant dependence of Nelsen's family 16 #

The generator is φ(u) = (θ/u + 1)(1 - u), and for u, v ∈ (0, 1] φ(uv) - φ(u) - φ(v) = (1 - u)(1 - v)(θ - uv) / (uv). Hence for θ ≥ 1 the copula is PQD, whereas for θ < 1 the diagonal point u = v = (1 + θ)/2 violates PQD. The copula is never NQD for θ > 0 (λ_L = 1/2), and θ = 0 is W. So the classification is: PQD iff θ ≥ 1, NQD iff θ = 0; for 0 < θ < 1 it is neither.

theorem ProbabilityTheory.Copula.isPQD_nelsen16 (θ : ℝ) (hθ : 1 ≤ θ) :
(nelsen16 θ ⋯).IsPQD

Nelsen's family 16 is PQD for θ ≥ 1.

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

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

theorem ProbabilityTheory.Copula.isPQD_nelsen16_iff (θ : ℝ) (hθ : 0 ≤ θ) :
(nelsen16 θ hθ).IsPQD ↔ 1 ≤ θ

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

theorem ProbabilityTheory.Copula.isNQD_nelsen16_iff (θ : ℝ) (hθ : 0 ≤ θ) :
(nelsen16 θ hθ).IsNQD ↔ θ = 0

Nelsen's family 16 is NQD iff θ = 0 (the lower Fréchet bound W).