← Mathematical handbook

theorem Papers.Rockel2026XiFootrule.ordinalSum_xi_eq_footrule_of_components (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (hC : C.chatterjeeXi = C.spearmanFootrule) (hD : D.chatterjeeXi = D.spearmanFootrule) : (C.ordinalSum D a).chatterjeeXi = (C.ordinalSum D a).spearmanFootrule

Rank equality is preserved by every binary ordinal sum, including endpoint splits.

theorem Papers.Rockel2026XiFootrule.ordinalSum_xi_eq_footrule_iff (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (hC : C.IsSI) (hD : D.IsSI) : (C.ordinalSum D a).chatterjeeXi = (C.ordinalSum D a).spearmanFootrule ↔ C.chatterjeeXi = C.spearmanFootrule ∧ D.chatterjeeXi = D.spearmanFootrule

For SI components and an interior split, equality of the sum forces equality in each block.

inductive Papers.Rockel2026XiFootrule.FinitePiOrdinal : ProbabilityTheory.Copula 2 → Prop

Finite recursively nested ordinal sums of independence and comonotonic blocks.

• independence : FinitePiOrdinal (ProbabilityTheory.Copula.independence 2)
• comonotonic : FinitePiOrdinal (ProbabilityTheory.Copula.comonotonic 2)
• ordinalSum {C D : ProbabilityTheory.Copula 2} (hC : FinitePiOrdinal C) (hD : FinitePiOrdinal D) (a : ↑unitInterval) : FinitePiOrdinal (C.ordinalSum D a)

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

Every finite nested ordinal sum of Π and M blocks is symmetric and has ξ=ψ.