← Mathematical handbook

Quadrant dependence and the signs of rank coefficients

theorem ProbabilityTheory.Copula.isPQD_iff_independence_le (C : Copula 2) : C.IsPQD ↔ ∀ (u : Fin 2 → ↑unitInterval), (independence 2).cdf u ≤ C.cdf u

theorem ProbabilityTheory.Copula.IsPQD.spearmanRho_nonneg {C : Copula 2} (h : C.IsPQD) : 0 ≤ C.spearmanRho

theorem ProbabilityTheory.Copula.IsPQD.spearmanFootrule_nonneg {C : Copula 2} (h : C.IsPQD) : 0 ≤ C.spearmanFootrule

theorem ProbabilityTheory.Copula.IsPQD.giniGamma_nonneg {C : Copula 2} (h : C.IsPQD) : 0 ≤ C.giniGamma

theorem ProbabilityTheory.Copula.IsPQD.blomqvistBeta_nonneg {C : Copula 2} (h : C.IsPQD) : 0 ≤ C.blomqvistBeta

theorem ProbabilityTheory.Copula.IsPQD.spearmanRho_le_three_mul_kendallTau {C : Copula 2} (h : C.IsPQD) : C.spearmanRho ≤ 3 * C.kendallTau

The PQD bound rho ≤ 3 tau, obtained by integrating uv ≤ C(u,v) against dC.

theorem ProbabilityTheory.Copula.IsPQD.kendallTau_nonneg {C : Copula 2} (h : C.IsPQD) : 0 ≤ C.kendallTau