← Mathematical handbook

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

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

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