← Mathematical handbook

theorem Verification.affine_product_integral (C : ProbabilityTheory.Copula 2) (a b w z : ℝ) : ∫ (x : Fin 2 → ↑unitInterval), (a + w * ↑(x 0)) * (b + z * ↑(x 1)) ∂C.toMeasure = (a + w / 2) * (b + z / 2) + w * z * C.spearmanRho / 12

theorem Verification.patchwork_rho_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).spearmanRho = 12 * ∑ i : Fin m, ∑ j : Fin n, A.mass i j * ((↑(P.point i.castSucc) + P.width i / 2) * (↑(Q.point j.castSucc) + Q.width j / 2) + P.width i * Q.width j * (C i j).spearmanRho / 12) - 3

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