← Mathematical handbook

theorem Papers.Rockel2026XiFootrule.countableOrdinal_cdf_section_eq_of_component_eq (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C D : ℕ → ProbabilityTheory.Copula 2) (k : ℕ) (v : ↑unitInterval) (hl : P.point k ≤ v) (hr : v ≤ P.point (k + 1)) (hk : C k = D k) (u : ↑unitInterval) : (ProbabilityTheory.Copula.countableOrdinalSum P C).cdf ![u, v] = (ProbabilityTheory.Copula.countableOrdinalSum P D).cdf ![u, v]

At a threshold inside one partition block, the CDF section depends only on that block's component.

theorem Papers.Rockel2026XiFootrule.countablePiM_isSI (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (hC : ∀ (k : ℕ), C k = ProbabilityTheory.Copula.independence 2 ∨ C k = ProbabilityTheory.Copula.comonotonic 2) : (ProbabilityTheory.Copula.countableOrdinalSum P C).IsSI

A countable adjacent sum of independence and comonotonic blocks is SI.

theorem Papers.Rockel2026XiFootrule.countablePiM_symmetric_si_rank_equality (P : ProbabilityTheory.Copula.CountableIntervalPartition) (C : ℕ → ProbabilityTheory.Copula 2) (hC : ∀ (k : ℕ), C k = ProbabilityTheory.Copula.independence 2 ∨ C k = ProbabilityTheory.Copula.comonotonic 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

Adjacent countable Π/M blocks realize symmetric SI equality cases.