← Mathematical handbook

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

Equations

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

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

The exact source matrix T T^T + T^T + I/3.

Equations

• Verification.checkerboardXiMatrix n = Verification.strictUpperMatrix n * (Verification.strictUpperMatrix n).transpose + (Verification.strictUpperMatrix n).transpose + (1 / 3) • 1

theorem Verification.trace_transpose_self_sum {m n : ℕ} (D : Matrix (Fin m) (Fin n) ℝ) : (D.transpose * D).trace = ∑ i : Fin m, ∑ j : Fin n, D i j ^ 2

theorem Verification.mass_mul_strictUpper {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (i : Fin m) (j : Fin n) : (Matrix.of A.mass * strictUpperMatrix n) i j = cellPrefix A i j

theorem Verification.checkerboardXi_trace {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 * checkerboardXiMatrix n).trace = ∑ i : Fin m, ∑ j : Fin n, (cellPrefix A i j ^ 2 + cellPrefix A i j * A.mass i j + A.mass i j ^ 2 / 3)