← Mathematical handbook

theorem Verification.checkerboard_rho_centers {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) : A.checkerboard.spearmanRho = 12 * ∑ i : Fin m, ∑ j : Fin n, A.mass i j * (1 - partitionCenter P i) * (1 - partitionCenter Q j) - 3

theorem Verification.uniform_patchwork_rho_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 : ProbabilityTheory.Copula 2) : (A.patchwork fun (x : Fin m) (x_1 : Fin n) => C).spearmanRho = A.checkerboard.spearmanRho + C.spearmanRho / (↑m * ↑n)

theorem Verification.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

The source Omega formula, for arbitrary admissible rectangular cell matrices.

theorem Verification.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 Verification.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)