Entrywise Matrix Product Trace Identity
ProvedFunctionalInequalities.Analysis.sum_matrix_product_entry_mul_eq_trace_readableThis statement is a finite-dimensional trace-algebra identity.
Let S,A,D be real matrices indexed by Fin n. Assume S and D are symmetric. Then
No symmetry assumption is imposed on A.
This identity converts an entrywise product of symmetric matrix expressions into a trace expression and is useful in finite trace-energy calculations.
Formalization Note All products are ordinary real matrix products over Fin n; the theorem is an equality, not an inequality.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.
theorem sum_matrix_product_entry_mul_eq_trace {n : ℕ}
(S A D : Matrix (Fin n) (Fin n) ℝ) (hS : S.IsSymm) (hD : D.IsSymm) :
(∑ p : Fin n × Fin n, (S * A * S) p.1 p.2 * (S * D * S) p.1 p.2) =
((S * S) * A * (S * S) * D).trace
Module navigation
Module: Analysis/Matrix/Trace/Algebra.
Previous: trace_mul_mul_mul_eq_sum · Next: sum_matrix_product_entry_quadratic_eq_trace.
Source excerpt, lines 121–124 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Trace_Algebra
theorem FunctionalInequalities.Analysis.sum_matrix_product_entry_mul_eq_trace_readable {n : ℕ}
(S A D : Matrix (Fin n) (Fin n) ℝ) (hS : S.IsSymm) (hD : D.IsSymm) :
(∑ p : Fin n × Fin n, (S * A * S) p.1 p.2 * (S * D * S) p.1 p.2) =
((S * S) * A * (S * S) * D).trace := by sorry