← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.boundary_trace_identity {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix α α ℝ) (B : Matrix β β ℝ) (D : Matrix α β ℝ) (a : α) (b : β) (hA : A + A.transpose = 2 • Matrix.single a a 1) (hB : B + B.transpose = 2 • Matrix.single b b 1) (hD : D a b = 1) : (A * D * B * D.transpose).trace + (A * D * B.transpose * D.transpose).trace = 2

The trace identity behind the Bernstein Kendall formula; only the symmetric boundary parts matter.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.trace_tensor_contraction {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (A : Matrix α α ℝ) (B : Matrix β β ℝ) (D : Matrix α β ℝ) : (A * D * B.transpose * D.transpose).trace = ∑ i : α, ∑ j : β, ∑ r : α, ∑ s : β, D i j * D r s * A i r * B j s