← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellMass_le_row {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (i : Fin m) (j : Fin n) : A.mass i j ≤ P.width i

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellMass_le_col {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (i : Fin m) (j : Fin n) : A.mass i j ≤ Q.width j

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellMass_square_bound {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (A : CellMass (IntervalPartition.uniform m hm) (IntervalPartition.uniform n hn)) : ∑ i : Fin m, ∑ j : Fin n, A.mass i j ^ 2 ≤ min (1 / ↑m) (1 / ↑n)