Weighted Matrix-Slice Trace Expansion

Proved

FunctionalInequalities.Analysis.letwin_trace_weighted_slices_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a finite matrix expansion identity.

For real $n\times n$ matrices $P,A,C$ and a family of matrices $V_a$ , one has

\sum_k\operatorname{tr}\left(A\left(\sum_aP_{ka}V_a\right)C\left(\sum_bP_{kb}V_b\right)\right) = \sum_{a,b}(P^{\mathsf T}P)_{ab}\operatorname{tr}(AV_aCV_b).

The statement is purely algebraic and is used to rewrite a sum of traces of weighted matrix slices.

Original Lean declaration header

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

private lemma letwin_trace_weighted_slices {n : ℕ}
    (P A C : Matrix (Fin n) (Fin n) ℝ)
    (V : Fin n → Matrix (Fin n) (Fin n) ℝ) :
    (∑ k, (A * (∑ a, P k a • V a) * C *
      (∑ b, P k b • V b)).trace) =
      ∑ a, ∑ b, (Pᵀ * P) a b * (A * V a * C * V b).trace

Module navigation

Module: Analysis/Matrix/Trace/Energy.

Previous: jordan_trace_domination · Next: letwin_tensor_trace_identity.

Source excerpt, lines 243–248 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Trace_Energy

open Matrix

Formal statement

 lemma FunctionalInequalities.Analysis.letwin_trace_weighted_slices_readable {n : ℕ}
    (P A C : Matrix (Fin n) (Fin n) ℝ)
    (V : Fin n → Matrix (Fin n) (Fin n) ℝ) :
    (∑ k, (A * (∑ a, P k a • V a) * C *
      (∑ b, P k b • V b)).trace) =
      ∑ a, ∑ b, (Pᵀ * P) a b * (A * V a * C * V b).trace := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Matrix/Trace/Energy.lean#L243-L290 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.Trace.Energy`, declaration `_private.FunctionalInequalities.Analysis.Matrix.Trace.Energy.0.FunctionalInequalities.Analysis.letwin_trace_weighted_slices`; the repository is private at upload time).

View graph