← Mathematical handbook

theorem Verification.partition_exists_Ioc {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (u : ↑unitInterval) (hu : 0 < u) : ∃ (i : Fin m), P.point i.castSucc < u ∧ u ≤ P.point i.succ

theorem Verification.partition_Ioc_index_mono {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) {i j : Fin m} {u v : ↑unitInterval} (hi : P.point i.castSucc < u ∧ u ≤ P.point i.succ) (hj : P.point j.castSucc < v ∧ v ≤ P.point j.succ) (huv : u ≤ v) : i ≤ j

theorem Verification.partitionPiece_of_mem {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (i r : Fin m) (u : ↑unitInterval) (hu : P.point r.castSucc < u ∧ u ≤ P.point r.succ) : partitionPiece P i (fun (x : ↑unitInterval) => 1) u = if i = r then 1 else 0

theorem Verification.checkerboardDensity_on_cell {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (i : Fin m) (j : Fin n) (u v : ↑unitInterval) (hu : P.point i.castSucc < u ∧ u ≤ P.point i.succ) (hv : Q.point j.castSucc < v ∧ v ≤ Q.point j.succ) : checkerboardDensity A ![u, v] = A.mass i j / (P.width i * Q.width j)

theorem Verification.checkerboardDensity_zero_left {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (v : ↑unitInterval) : checkerboardDensity A ![0, v] = 0

theorem Verification.checkerboardDensity_zero_right {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (u : ↑unitInterval) : checkerboardDensity A ![u, 0] = 0

theorem Verification.checkerboard_hasMTP2Density {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (hA : ProbabilityTheory.IsTP2 A.mass) : A.checkerboard.HasMTP2Density

Every TP2 cell-mass matrix yields an MTP2 Lebesgue density, including zero entries.