← Copula mathematical handbook

Criteria for quadrant dependence of Archimedean copulas

For a bivariate Archimedean generator g with inverse generator ψ = g.toFun (Nelsen, An Introduction to Copulas, second edition, Section 4.4 with C₂ = Π), we prove two-sided criteria that do not need strictness of ψ:

• isPQD_of_psi / not_isPQD_of_psi: C is PQD as soon as ψ(x) ψ(y) ≤ ψ(x + y) for all x, y ≥ 0, and it is not PQD as soon as ψ(x + y) < ψ(x) ψ(y) for one pair;
• isNQD_of_psi / not_isNQD_of_psi: the reverse inequalities give NQD and non-NQD;
• isPQD_of_phi / not_isPQD_of_phi: the same statements in terms of the generator φ, φ(u) + φ(v) ≤ φ(u v);
• not_isNQD_of_hasLowerTailDependence, not_isNQD_of_hasUpperTailDependence: a nonzero tail coefficient excludes NQD;
• isNQD_reflect_iff, isPQD_reflect_iff: reflecting the second coordinate swaps PQD and NQD.

theorem ProbabilityTheory.Copula.BivariateGenerator.invFunReal_of_pos (g : BivariateGenerator) {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : g.invFunReal x = g.invFun ⟨x, ⋯⟩

On (0, 1] the real extension invFunReal agrees with invFun.

theorem ProbabilityTheory.Copula.BivariateGenerator.toFun_invFunReal (g : BivariateGenerator) {x : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) : g.toFun (g.invFunReal x) = x

ψ (φ x) = x on (0, 1], for the real extension invFunReal.

theorem ProbabilityTheory.Copula.BivariateGenerator.isPQD_of_psi (g : BivariateGenerator) (h : ∀ (x y : ℝ), 0 ≤ x → 0 ≤ y → g.toFun x * g.toFun y ≤ g.toFun (x + y)) : g.copula.IsPQD

Sufficient criterion for PQD: ψ(x) ψ(y) ≤ ψ(x + y) for all x, y ≥ 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.isNQD_of_psi (g : BivariateGenerator) (h : ∀ (x y : ℝ), 0 ≤ x → 0 ≤ y → g.toFun (x + y) ≤ g.toFun x * g.toFun y) : g.copula.IsNQD

Sufficient criterion for NQD: ψ(x + y) ≤ ψ(x) ψ(y) for all x, y ≥ 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.not_isPQD_of_psi (g : BivariateGenerator) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (h : g.toFun (x + y) < g.toFun x * g.toFun y) : ¬g.copula.IsPQD

A pair x, y ≥ 0 with ψ(x + y) < ψ(x) ψ(y) shows that C is not PQD.

theorem ProbabilityTheory.Copula.BivariateGenerator.not_isNQD_of_psi (g : BivariateGenerator) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (h : g.toFun x * g.toFun y < g.toFun (x + y)) : ¬g.copula.IsNQD

A pair x, y ≥ 0 with ψ(x) ψ(y) < ψ(x + y) shows that C is not NQD.

theorem ProbabilityTheory.Copula.BivariateGenerator.isPQD_iff_psi (g : BivariateGenerator) : g.copula.IsPQD ↔ ∀ (x y : ℝ), 0 ≤ x → 0 ≤ y → g.toFun x * g.toFun y ≤ g.toFun (x + y)

PQD is equivalent to ψ(x) ψ(y) ≤ ψ(x + y) for all x, y ≥ 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.isNQD_iff_psi (g : BivariateGenerator) : g.copula.IsNQD ↔ ∀ (x y : ℝ), 0 ≤ x → 0 ≤ y → g.toFun (x + y) ≤ g.toFun x * g.toFun y

NQD is equivalent to ψ(x + y) ≤ ψ(x) ψ(y) for all x, y ≥ 0.

theorem ProbabilityTheory.Copula.BivariateGenerator.isNQD_innerPower (g : BivariateGenerator) (q : ℝ) (hq : 1 ≤ q) (h : g.copula.IsNQD) : (g.innerPower q hq).copula.IsNQD

Inner powers ψ ^ q (q ≥ 1) preserve NQD.

theorem ProbabilityTheory.Copula.BivariateGenerator.isPQD_innerPower (g : BivariateGenerator) (q : ℝ) (hq : 1 ≤ q) (h : g.copula.IsPQD) : (g.innerPower q hq).copula.IsPQD

Inner powers ψ ^ q (q ≥ 1) preserve PQD.

theorem ProbabilityTheory.Copula.BivariateGenerator.isPQD_of_phi (g : BivariateGenerator) (h : ∀ (u v : ℝ), 0 < u → u ≤ 1 → 0 < v → v ≤ 1 → g.invFunReal u + g.invFunReal v ≤ g.invFunReal (u * v)) : g.copula.IsPQD

Sufficient criterion for PQD in terms of the generator: φ(u) + φ(v) ≤ φ(u v).

theorem ProbabilityTheory.Copula.BivariateGenerator.not_isPQD_of_phi (g : BivariateGenerator) {u v : ℝ} (hu0 : 0 < u) (hu1 : u ≤ 1) (hv0 : 0 < v) (hv1 : v ≤ 1) (h : g.invFunReal (u * v) < g.invFunReal u + g.invFunReal v) : ¬g.copula.IsPQD

If φ(u v) < φ(u) + φ(v) for some u, v ∈ (0, 1], then C is not PQD.

theorem ProbabilityTheory.Copula.not_isNQD_of_hasLowerTailDependence {C : Copula 2} {l : ℝ} (h : C.HasLowerTailDependence l) (hl : l ≠ 0) : ¬C.IsNQD

A nonzero lower tail coefficient excludes NQD.

theorem ProbabilityTheory.Copula.not_isNQD_of_hasUpperTailDependence {C : Copula 2} {l : ℝ} (h : C.HasUpperTailDependence l) (hl : l ≠ 0) : ¬C.IsNQD

A nonzero upper tail coefficient excludes NQD.

theorem ProbabilityTheory.Copula.isNQD_reflect_of_isPQD {C : Copula 2} (h : C.IsPQD) : (C.reflect {1}).IsNQD

Reflecting the second coordinate turns PQD into NQD.

theorem ProbabilityTheory.Copula.isPQD_reflect_of_isNQD {C : Copula 2} (h : C.IsNQD) : (C.reflect {1}).IsPQD

Reflecting the second coordinate turns NQD into PQD.

theorem ProbabilityTheory.Copula.not_isPQD_reflect_of_not_isNQD {C : Copula 2} (h : ¬C.IsNQD) : ¬(C.reflect {1}).IsPQD

If C is not NQD, its second-coordinate reflection is not PQD.

theorem ProbabilityTheory.Copula.not_isNQD_reflect_of_not_isPQD {C : Copula 2} (h : ¬C.IsPQD) : ¬(C.reflect {1}).IsNQD

If C is not PQD, its second-coordinate reflection is not NQD.