← Mathematical handbook

theorem Verification.copulaRowMean_mono {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (C : ProbabilityTheory.Copula 2) (i : Fin m) : Monotone (copulaRowMean P C i)

theorem Verification.copulaRowMean_total {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : ∑ i : Fin m, P.width i * copulaRowMean P C i v = ↑v

theorem Verification.checkerboardRow_interpolation_error {m n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (i : Fin m) (j : Fin n) (v : ↑unitInterval) : |checkerboardRow (C.cellMass P Q) i (partitionEmbed Q j v) - copulaRowMean P C i (partitionEmbed Q j v)| ≤ copulaRowMean P C i (Q.point j.succ) - copulaRowMean P C i (Q.point j.castSucc)

theorem Verification.checkerboard_energy_interpolation_error_embed {m n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (j : Fin n) (v : ↑unitInterval) : |conditionalEnergy (C.cellMass P Q).checkerboard (partitionEmbed Q j v) - rowMeanEnergy P C (partitionEmbed Q j v)| ≤ 2 * Q.width j

theorem Verification.partitionEmbed_exists {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (v : ↑unitInterval) : ∃ (i : Fin m) (u : ↑unitInterval), partitionEmbed P i u = v

theorem Verification.checkerboard_energy_interpolation_error {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (C : ProbabilityTheory.Copula 2) (n : ℕ) (v : ↑unitInterval) : |conditionalEnergy (C.cellMass P (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)).checkerboard v - rowMeanEnergy P C v| ≤ 2 / (↑n + 1)