← Mathematical handbook

theorem Papers.Rockel2026XiFootrule.countablePi_exchangeable (P : ProbabilityTheory.Copula.CountableIntervalPartition) : (ProbabilityTheory.Copula.countableOrdinalSumPi P).IsExchangeable

Adjacent countable ordinal sums of independence blocks remain symmetric.

theorem Papers.Rockel2026XiFootrule.countablePi_diagonal_fixed (P : ProbabilityTheory.Copula.CountableIntervalPartition) (n : ℕ) : (ProbabilityTheory.Copula.countableOrdinalSumPi P).diagonal (P.point n) = ↑(P.point n)

Every partition endpoint is a diagonal fixed point of the countable sum.

theorem Papers.Rockel2026XiFootrule.countablePi_has_binary_split (P : ProbabilityTheory.Copula.CountableIntervalPartition) (n : ℕ) : ∃ (C : ProbabilityTheory.Copula 2) (D : ProbabilityTheory.Copula 2), C.ordinalSum D (P.point (n + 1)) = ProbabilityTheory.Copula.countableOrdinalSumPi P

Every positive endpoint determines a genuine binary ordinal-sum decomposition.

theorem Papers.Rockel2026XiFootrule.countablePi_first_lower_component (P : ProbabilityTheory.Copula.CountableIntervalPartition) : (ProbabilityTheory.Copula.countableOrdinalSumPi P).lowerOrdinalComponent (P.point 1) ⋯ ⋯ = ProbabilityTheory.Copula.independence 2

The first rescaled component of a countable Pi-block sum is exactly Pi.