← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.strictUpperMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.strictUpperMatrix n = Matrix.of fun (i j : Fin n) => if i < j then 1 else 0

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboardXiMatrix (n : ℕ) : Matrix (Fin n) (Fin n) ℝ

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

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.mass_mul_strictUpper {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (i : Fin m) (j : Fin n) : (Matrix.of A.mass * strictUpperMatrix n) i j = cellPrefix A i j

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.checkerboardXi_trace {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : 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)