← Mathematical handbook

Proposition 3.3(iii) and Corollary 3.4 on arbitrary rectangular grids

theorem Papers.Rockel2025Approximation.patchwork_conditionalCDF {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (C : Fin m → Fin n → ProbabilityTheory.Copula 2) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (A.patchwork C).conditionalCDF u v) =ᵐ[MeasureTheory.volume] Verification.patchworkKernel A C v

theorem Papers.Rockel2025Approximation.patchwork_xi_formula {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (C : Fin m → Fin n → ProbabilityTheory.Copula 2) : (A.patchwork C).chatterjeeXi = 6 * ∑ i : Fin m, P.width i * ∑ j : Fin n, Q.width j * ((Verification.cellPrefix A i j / P.width i) ^ 2 + Verification.cellPrefix A i j / P.width i * (A.mass i j / P.width i) + (A.mass i j / P.width i) ^ 2 * ((C i j).chatterjeeXi + 2) / 6) - 2

theorem Papers.Rockel2025Approximation.patchwork_xi_correction {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (C : Fin m → Fin n → ProbabilityTheory.Copula 2) : (A.patchwork C).chatterjeeXi = A.checkerboard.chatterjeeXi + ∑ i : Fin m, ∑ j : Fin n, Q.width j / P.width i * A.mass i j ^ 2 * (C i j).chatterjeeXi

theorem Papers.Rockel2025Approximation.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 * Verification.checkerboardXiMatrix n).trace - 2

theorem Papers.Rockel2025Approximation.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 Papers.Rockel2025Approximation.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 Papers.Rockel2025Approximation.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 Papers.Rockel2025Approximation.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 Papers.Rockel2025Approximation.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