Schur comparison bounds the CDF by a stochastically monotone comparator #
theorem
Verification.lowerOrthantLE_of_schurLE_isSI
(C D : ProbabilityTheory.Copula 2)
(h : C.SchurLE D)
(hD : D.IsSI)
:
C.LowerOrthantLE D
Lemma 2.6(i): no monotonicity hypothesis is required on the smaller copula.
theorem
Verification.lowerOrthantLE_of_schurLE_isSD
(C D : ProbabilityTheory.Copula 2)
(h : C.SchurLE D)
(hD : D.IsSD)
:
D.LowerOrthantLE C
Lemma 2.8(i) follows by reflecting the response coordinate.