← Mathematical handbook

theorem Verification.rectangular_checkerboard_xi {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn)) : A.checkerboard.chatterjeeXi = 6 * ↑m / ↑n * ((Matrix.of A.mass).transpose * Matrix.of A.mass * checkerboardXiMatrix n).trace - 2

theorem Verification.uniform_patchwork_xi_correction {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn)) (C : Fin m → Fin n → ProbabilityTheory.Copula 2) : (A.patchwork C).chatterjeeXi = A.checkerboard.chatterjeeXi + ↑m / ↑n * ∑ i : Fin m, ∑ j : Fin n, A.mass i j ^ 2 * (C i j).chatterjeeXi

theorem Verification.rectangular_perfect_xi {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn)) (C : Fin m → Fin n → ProbabilityTheory.Copula 2) (hC : ∀ (i : Fin m) (j : Fin n), (C i j).chatterjeeXi = 1) : (A.patchwork C).chatterjeeXi = A.checkerboard.chatterjeeXi + ↑m / ↑n * ((Matrix.of A.mass).transpose * Matrix.of A.mass).trace

theorem Verification.rectangular_checkMin_xi {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn)) : A.checkMin.chatterjeeXi = A.checkerboard.chatterjeeXi + ↑m / ↑n * ((Matrix.of A.mass).transpose * Matrix.of A.mass).trace

theorem Verification.rectangular_checkW_xi {m n : ℕ} (hm : 0 < m) (hn : 0 < n) (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform m hm) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn)) : A.checkW.chatterjeeXi = A.checkerboard.chatterjeeXi + ↑m / ↑n * ((Matrix.of A.mass).transpose * Matrix.of A.mass).trace

theorem Verification.rectangular_xi_error_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)) (C : Fin m → Fin n → ProbabilityTheory.Copula 2) : |(A.patchwork C).chatterjeeXi - A.checkerboard.chatterjeeXi| ≤ if m ≤ n then ↑m / ↑n ^ 2 else 1 / ↑n

Corollary 3.4, in fact valid for every choice of local copulas.