Schur comparison in both coordinate directions #
This distinguishes the paper's two-direction comparison from the directional
SchurLE used for Chatterjee's xi.
theorem
ProbabilityTheory.Copula.SchurBothLE.trans
{C D E : Copula 2}
(h : C.SchurBothLE D)
(k : D.SchurBothLE E)
:
C.SchurBothLE E
@[simp]
theorem
ProbabilityTheory.Copula.schurBothLE_iff_of_exchangeable
{C D : Copula 2}
(hC : C.IsExchangeable)
(hD : D.IsExchangeable)
:
theorem
ProbabilityTheory.Copula.schurBothLE_iff_of_archimedean
{C D : Copula 2}
(hC : C.IsArchimedean)
(hD : D.IsArchimedean)
: