← Mathematical handbook

theorem Verification.checkerboardRow_mem {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (i : Fin m) (v : ↑unitInterval) : checkerboardRow A i v ∈ Set.Icc 0 1

theorem Verification.copulaRowMean_sub_le {m : ℕ} (C D : ProbabilityTheory.Copula 2) (P : ProbabilityTheory.Copula.IntervalPartition m) (ε : ℝ) (h : ∀ (u v : ↑unitInterval), |C.cdf ![u, v] - D.cdf ![u, v]| ≤ ε) (i : Fin m) (v : ↑unitInterval) : |copulaRowMean P C i v - copulaRowMean P D i v| ≤ 2 * ε / P.width i

theorem Verification.checkerboardRow_sub_le_embed {m n : ℕ} (C D : ProbabilityTheory.Copula 2) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (ε : ℝ) (h : ∀ (u v : ↑unitInterval), |C.cdf ![u, v] - D.cdf ![u, v]| ≤ ε) (i : Fin m) (j : Fin n) (v : ↑unitInterval) : |checkerboardRow (C.cellMass P Q) i (partitionEmbed Q j v) - checkerboardRow (D.cellMass P Q) i (partitionEmbed Q j v)| ≤ 2 * ε / P.width i

theorem Verification.sq_sub_le_of_mem_unit {a b δ : ℝ} (ha : a ∈ Set.Icc 0 1) (_hb : b ∈ Set.Icc 0 1) (hδ : |a - b| ≤ δ) : a ^ 2 ≤ b ^ 2 + 2 * δ

theorem Verification.checkerboard_energy_stability_embed {m n : ℕ} (C D : ProbabilityTheory.Copula 2) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (ε : ℝ) (h : ∀ (u v : ↑unitInterval), |C.cdf ![u, v] - D.cdf ![u, v]| ≤ ε) (j : Fin n) (v : ↑unitInterval) : conditionalEnergy (C.cellMass P Q).checkerboard (partitionEmbed Q j v) ≤ conditionalEnergy (D.cellMass P Q).checkerboard (partitionEmbed Q j v) + 4 * ↑m * ε

theorem Verification.checkerboard_xi_stability_le {m n : ℕ} (C D : ProbabilityTheory.Copula 2) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (ε : ℝ) (h : ∀ (u v : ↑unitInterval), |C.cdf ![u, v] - D.cdf ![u, v]| ≤ ε) : (C.cellMass P Q).checkerboard.chatterjeeXi ≤ (D.cellMass P Q).checkerboard.chatterjeeXi + 24 * ↑m * ε

theorem Verification.checkerboard_xi_stability {m n : ℕ} (C D : ProbabilityTheory.Copula 2) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (ε : ℝ) (h : ∀ (u v : ↑unitInterval), |C.cdf ![u, v] - D.cdf ![u, v]| ≤ ε) : |(C.cellMass P Q).checkerboard.chatterjeeXi - (D.cellMass P Q).checkerboard.chatterjeeXi| ≤ 24 * ↑m * ε

Stability on arbitrary partitions; the constant depends only on the number of predictor bins.