← Mathematical handbook

noncomputable def Verification.checkerXiMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℝ

The source Xi matrix has 2 below the diagonal, 1 on it and 0 above it.

Equations

• Verification.checkerXiMatrix n = Matrix.of fun (i r : Fin n) => if r < i then 2 else if r = i then 1 else 0

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

theorem Verification.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 - (checkerXiMatrix m * Matrix.of A.mass * checkerXiMatrix n * (Matrix.of A.mass).transpose).trace

theorem Verification.cellMass_frobenius {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) : ((Matrix.of A.mass).transpose * Matrix.of A.mass).trace = ∑ i : Fin m, ∑ j : Fin n, A.mass i j ^ 2

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