Documentation

Copula.Order.Rank

← Copula mathematical handbook

Concordance order and rank coefficients #

theorem ProbabilityTheory.Copula.integral_cdf_swap (C D : Copula 2) :

∫ (x : Fin 2 → ↑unitInterval), C.cdf x ∂D.toMeasure = ∫ (x : Fin 2 → ↑unitInterval), D.cdf x ∂C.toMeasure

The bivariate cross-concordance integral is symmetric.

theorem ProbabilityTheory.Copula.LowerOrthantLE.kendallTau_le {C D : Copula 2} (h : C.LowerOrthantLE D) :

C.kendallTau ≤ D.kendallTau

theorem ProbabilityTheory.Copula.LowerOrthantLE.spearmanRho_le {C D : Copula 2} (h : C.LowerOrthantLE D) :

C.spearmanRho ≤ D.spearmanRho

theorem ProbabilityTheory.Copula.LowerOrthantLE.spearmanFootrule_le {C D : Copula 2} (h : C.LowerOrthantLE D) :

C.spearmanFootrule ≤ D.spearmanFootrule

theorem ProbabilityTheory.Copula.LowerOrthantLE.giniGamma_le {C D : Copula 2} (h : C.LowerOrthantLE D) :

C.giniGamma ≤ D.giniGamma

theorem ProbabilityTheory.Copula.LowerOrthantLE.blomqvistBeta_le {C D : Copula 2} (h : C.LowerOrthantLE D) :

C.blomqvistBeta ≤ D.blomqvistBeta

theorem ProbabilityTheory.Copula.isPQD_iff_lowerOrthantLE (C : Copula 2) :

C.IsPQD ↔ (independence 2).LowerOrthantLE C

theorem ProbabilityTheory.Copula.lowerOrthantLE_countermonotonic (C : Copula 2) :

countermonotonic.LowerOrthantLE C

theorem ProbabilityTheory.Copula.lowerOrthantLE_comonotonic (C : Copula 2) :

C.LowerOrthantLE (comonotonic 2)

theorem ProbabilityTheory.Copula.concordanceLE_countermonotonic (C : Copula 2) :

countermonotonic.ConcordanceLE C

theorem ProbabilityTheory.Copula.concordanceLE_comonotonic (C : Copula 2) :

C.ConcordanceLE (comonotonic 2)