← Mathematical handbook

theorem Papers.Rockel2026XiFootrule.ordinalSum_isSI (C D : ProbabilityTheory.Copula 2) (hC : C.IsSI) (hD : D.IsSI) (a : ↑unitInterval) : (C.ordinalSum D a).IsSI

Binary ordinal sums preserve stochastic increase, including endpoint splits.

theorem Papers.Rockel2026XiFootrule.FinitePiOrdinal.isSI {C : ProbabilityTheory.Copula 2} (h : FinitePiOrdinal C) : C.IsSI

Every finite nested ordinal sum of independence and comonotonic blocks is SI.

theorem Papers.Rockel2026XiFootrule.FinitePiOrdinal.symmetric_si_rank_equality {C : ProbabilityTheory.Copula 2} (h : FinitePiOrdinal C) : C.IsSI ∧ C.IsExchangeable ∧ C.chatterjeeXi = C.spearmanFootrule

The finite part of the symmetric SI equality construction.