← Mathematical handbook

noncomputable def Verification.checkerboardRow {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (i : Fin m) (v : ↑unitInterval) : ℝ

Equations

• Verification.checkerboardRow A i v = ∑ j : Fin n, A.mass i j / P.width i * ↑(Q.coord j v)

theorem Verification.cellMass_row_prefix {m n : ℕ} (C : ProbabilityTheory.Copula 2) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin m) (k : Fin (n + 1)) : (∑ j : Fin n, if ↑j < ↑k then (C.cellMass P Q).mass i j else 0) = C.cdf ![P.point i.succ, Q.point k] - C.cdf ![P.point i.castSucc, Q.point k]

theorem Verification.checkerboardRow_grid {m n : ℕ} (C : ProbabilityTheory.Copula 2) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (i : Fin m) (k : Fin (n + 1)) : checkerboardRow (C.cellMass P Q) i (Q.point k) = copulaRowMean P C i (Q.point k)

theorem Verification.partition_coord_embed_affine {n : ℕ} (Q : ProbabilityTheory.Copula.IntervalPartition n) (j s : Fin n) (v : ↑unitInterval) : ↑(Q.coord s (partitionEmbed Q j v)) = (1 - ↑v) * ↑(Q.coord s (Q.point j.castSucc)) + ↑v * ↑(Q.coord s (Q.point j.succ))

theorem Verification.checkerboardRow_embed {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (i : Fin m) (j : Fin n) (v : ↑unitInterval) : checkerboardRow A i (partitionEmbed Q j v) = (1 - ↑v) * checkerboardRow A i (Q.point j.castSucc) + ↑v * checkerboardRow A i (Q.point j.succ)