Tensor Trace Expansion Identity

This is a finite-dimensional tensor trace identity.

Let $G,M$ be real $n\times n$ matrices with $M^{\mathsf T}=M$, and let $T_{abc}$ satisfy symmetry in its last two indices, $T_{abc}=T_{acb}$. Then

where $(T_a)_{ij}=T_{aij}$. This identity expands the trace expression into coordinate sums for the tensor comparison argument.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

private lemma letwin_tensor_trace_identity {n : ℕ}
    (G M : Matrix (Fin n) (Fin n) ℝ) (hM : Mᵀ = M)
    (T : Fin n → Fin n → Fin n → ℝ)
    (hT : ∀ a b c, T a b c = T a c b) :
    (∑ a, ∑ c, G a c *
      (M * Matrix.of (fun i j => T a i j) * G *
        Matrix.of (fun i j => T c i j)).trace) =
      ∑ i, ∑ j, M i j *
        ∑ a, ∑ b, ∑ c, ∑ d, G a c * G b d * T a b i * T c d j

Module navigation

Module: Analysis/Matrix/Trace/Energy.

Previous: letwin_trace_weighted_slices · Next: letwin_tensor_comparison.

Source excerpt, lines 318–326 · Frozen source 408915f.