Nonnegative Trace Of A Product
ProvedFunctionalInequalities.Analysis.trace_mul_nonneg_readablefunctional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave
This formalizes part of Theorem 2.5 of Letwin (arXiv:2607.24164v1), cited there as the key moment-map Hessian bound.
Let ι be a finite index type, and let A and C be real positive semidefinite matrices indexed by ι. Then the trace of their product is nonnegative:
The product AC itself is not asserted to be positive semidefinite.
This elementary trace-pairing fact is reusable whenever two positive semidefinite matrix fields produce a cross term.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.
theorem trace_mul_nonneg {ι : Type*} [Fintype ι]
{A C : Matrix ι ι ℝ} (hA : A.PosSemidef) (hC : C.PosSemidef) :
0 ≤ (A * C).trace
Module navigation
Module: Analysis/Matrix/Positivity.
Previous: inverse_quadratic_young · Next: traceGram_posSemidef.
Source excerpt, lines 366–368 · Frozen source 408915f.
Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Positivity
Formal statement
theorem FunctionalInequalities.Analysis.trace_mul_nonneg_readable {ι : Type*} [Fintype ι]
{A C : Matrix ι ι ℝ} (hA : A.PosSemidef) (hC : C.PosSemidef) :
0 ≤ (A * C).trace := by sorry
Source
Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Theorem 2.5. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Matrix/Positivity.lean#L364-L382 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.Positivity`, declaration `FunctionalInequalities.Analysis.trace_mul_nonneg`; the repository is private at upload time).