Entrywise Quadratic Energy Trace Identity
ProvedFunctionalInequalities.Analysis.sum_matrix_product_entry_quadratic_eq_trace_readableThis statement converts a family of entrywise quadratic energies into a trace sum.
Let S be a symmetric real n-by-n matrix. Let R be an arbitrary real m-by-m matrix, and let Tₖ be symmetric real n-by-n matrices indexed by Fin m. For each pair of matrix-entry indices p, define the vector whose k-th coordinate is . Then
This is a finite algebraic identity for entrywise inverse-quadratic energies and trace energies.
Formalization Note R need not be symmetric or positive; symmetry is required only for S and every Tₖ.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.
theorem sum_matrix_product_entry_quadratic_eq_trace {m n : ℕ}
(S : Matrix (Fin n) (Fin n) ℝ) (hS : S.IsSymm)
(R : Matrix (Fin m) (Fin m) ℝ)
(T : Fin m → Matrix (Fin n) (Fin n) ℝ) (hT : ∀ k, (T k).IsSymm) :
(∑ p : Fin n × Fin n,
(fun k => (S * T k * S) p.1 p.2) ⬝ᵥ
(R *ᵥ (fun k => (S * T k * S) p.1 p.2))) =
∑ k : Fin m, ∑ l : Fin m, R k l * ((S * S) * T k * (S * S) * T l).trace
Module navigation
Module: Analysis/Matrix/Trace/Algebra.
Supporting theorems: sum_matrix_product_entry_mul_eq_trace.
Previous: sum_matrix_product_entry_mul_eq_trace.
Source excerpt, lines 148–155 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Trace_Algebra open Matrix set_option maxHeartbeats 1000000
theorem FunctionalInequalities.Analysis.sum_matrix_product_entry_quadratic_eq_trace_readable {m n : ℕ}
(S : Matrix (Fin n) (Fin n) ℝ) (hS : S.IsSymm)
(R : Matrix (Fin m) (Fin m) ℝ)
(T : Fin m → Matrix (Fin n) (Fin n) ℝ) (hT : ∀ k, (T k).IsSymm) :
(∑ p : Fin n × Fin n,
(fun k => (S * T k * S) p.1 p.2) ⬝ᵥ
(R *ᵥ (fun k => (S * T k * S) p.1 p.2))) =
∑ k : Fin m, ∑ l : Fin m, R k l * ((S * S) * T k * (S * S) * T l).trace := by sorry