Trace Expansion for Four Matrix Factors

This is an algebraic expansion of the trace of a product of four real square matrices.

Let $n$ be a natural number and let $A,H,B,J$ be matrices in $M_n(\mathbb R)$. Then:

The Lean definition involved is trace_mul_mul_mul_eq_sum_readable. This identity is a reusable coordinate formula for trace quartics and does not require symmetry, invertibility, or positivity of any matrix.

Original Lean declaration header

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

theorem trace_mul_mul_mul_eq_sum {n : ℕ} (A H B J : Matrix (Fin n) (Fin n) ℝ) :
    (A * H * B * J).trace =
      ∑ q : Fin n × Fin n × Fin n × Fin n,
        (A q.1 q.2.1 * B q.2.2.1 q.2.2.2) *
          (H q.2.1 q.2.2.1 * J q.2.2.2 q.1)

Module navigation

Module: Analysis/Matrix/Trace/Algebra.

Next: sum_matrix_product_entry_mul_eq_trace.

Source excerpt, lines 88–92 · Frozen source 408915f.