← Mathematical handbook

Proposition 3.3(i)-(ii) for arbitrary rectangular cell matrices

theorem Papers.Rockel2025Approximation.rectangular_checkerboard_rho {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.spearmanRho = 3 * ∑ i : Fin m, ∑ j : Fin n, (2 * ↑m - 2 * (↑↑i + 1) + 1) * (2 * ↑n - 2 * (↑↑j + 1) + 1) / (↑m * ↑n) * A.mass i j - 3

theorem Papers.Rockel2025Approximation.rectangular_checkMin_rho {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.spearmanRho = A.checkerboard.spearmanRho + 1 / (↑m * ↑n)

theorem Papers.Rockel2025Approximation.rectangular_checkW_rho {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.spearmanRho = A.checkerboard.spearmanRho - 1 / (↑m * ↑n)

theorem Papers.Rockel2025Approximation.rectangular_checkerboard_tau {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) : A.checkerboard.kendallTau = 1 - (Verification.checkerXiMatrix m * Matrix.of A.mass * Verification.checkerXiMatrix n * (Matrix.of A.mass).transpose).trace

theorem Papers.Rockel2025Approximation.rectangular_checkMin_tau {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) : A.checkMin.kendallTau = A.checkerboard.kendallTau + ((Matrix.of A.mass).transpose * Matrix.of A.mass).trace

theorem Papers.Rockel2025Approximation.rectangular_checkW_tau {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) : A.checkW.kendallTau = A.checkerboard.kendallTau - ((Matrix.of A.mass).transpose * Matrix.of A.mass).trace

theorem Papers.Rockel2025Approximation.patchwork_rho_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).spearmanRho = A.checkerboard.spearmanRho + ∑ i : Fin m, ∑ j : Fin n, A.mass i j * P.width i * Q.width j * (C i j).spearmanRho

theorem Papers.Rockel2025Approximation.patchwork_tau_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).kendallTau = A.checkerboard.kendallTau + ∑ i : Fin m, ∑ j : Fin n, A.mass i j ^ 2 * (C i j).kendallTau