← Copula mathematical handbook

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

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

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchwork_tau_correction {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rectangular_checkerboard_tau {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) : A.checkerboard.kendallTau = 1 - (checkerXiMatrix m * Matrix.of A.mass * checkerXiMatrix n * (Matrix.of A.mass).transpose).trace

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellMass_frobenius {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rectangular_checkMin_tau {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) : A.checkMin.kendallTau = A.checkerboard.kendallTau + ((Matrix.of A.mass).transpose * Matrix.of A.mass).trace

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rectangular_checkW_tau {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) : A.checkW.kendallTau = A.checkerboard.kendallTau - ((Matrix.of A.mass).transpose * Matrix.of A.mass).trace