← Mathematical handbook

theorem Papers.Rockel2026XiFootrule.countableOrdinal_isSI (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (hC : ∀ (k : ℕ), (C k).IsSI) : (ProbabilityTheory.Copula.countableOrdinalSum P C).IsSI

Adjacent countable ordinal sums preserve stochastic increase for arbitrary SI component copulas, not just independence/comonotonic blocks.

theorem Papers.Rockel2026XiFootrule.ordinalSum_isSI_components (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (h : (C.ordinalSum D a).IsSI) : C.IsSI ∧ D.IsSI

SI of an interior binary ordinal sum forces SI in each rescaled component.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_isSI_iff (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) : (ProbabilityTheory.Copula.countableOrdinalSum P C).IsSI ↔ ∀ (k : ℕ), (C k).IsSI

For an adjacent countable partition, the sum is SI exactly when every component is SI.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_symmetric_si_rank_equality (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (hC : ∀ (k : ℕ), (C k).IsSI ∧ (C k).IsExchangeable ∧ (C k).chatterjeeXi = (C k).spearmanFootrule) : (ProbabilityTheory.Copula.countableOrdinalSum P C).IsSI ∧ (ProbabilityTheory.Copula.countableOrdinalSum P C).IsExchangeable ∧ (ProbabilityTheory.Copula.countableOrdinalSum P C).chatterjeeXi = (ProbabilityTheory.Copula.countableOrdinalSum P C).spearmanFootrule

Symmetry, SI, and rank equality pass from every block to an adjacent countable ordinal sum.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_xi_eq_footrule_iff (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (hSI : ∀ (k : ℕ), (C k).IsSI) : (ProbabilityTheory.Copula.countableOrdinalSum P C).chatterjeeXi = (ProbabilityTheory.Copula.countableOrdinalSum P C).spearmanFootrule ↔ ∀ (k : ℕ), (C k).chatterjeeXi = (C k).spearmanFootrule

In the adjacent countable SI class, equality ξ=ψ holds exactly when it holds in every component.

theorem Papers.Rockel2026XiFootrule.ordinalSum_exchangeable_components (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) (h : (C.ordinalSum D a).IsExchangeable) : C.IsExchangeable ∧ D.IsExchangeable

Exchangeability of an interior binary ordinal sum forces symmetry of both blocks.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_exchangeable_iff (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) : (ProbabilityTheory.Copula.countableOrdinalSum P C).IsExchangeable ↔ ∀ (k : ℕ), (C k).IsExchangeable

Exchangeability of an adjacent countable ordinal sum is equivalent to exchangeability of each component.

theorem Papers.Rockel2026XiFootrule.countableOrdinal_symmetric_si_rank_equality_iff (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) : (ProbabilityTheory.Copula.countableOrdinalSum P C).IsSI ∧ (ProbabilityTheory.Copula.countableOrdinalSum P C).IsExchangeable ∧ (ProbabilityTheory.Copula.countableOrdinalSum P C).chatterjeeXi = (ProbabilityTheory.Copula.countableOrdinalSum P C).spearmanFootrule ↔ ∀ (k : ℕ), (C k).IsSI ∧ (C k).IsExchangeable ∧ (C k).chatterjeeXi = (C k).spearmanFootrule

Complete componentwise SI/symmetry/rank-equality criterion for the adjacent countable ordinal-sum constructor.