Positive Semidefinite Trace Gram Matrix
ProvedFunctionalInequalities.Analysis.traceGram_posSemidef_readableThis formalizes part of Theorem 2.5 of Letwin (arXiv:2607.24164v1), cited there as the key moment-map Hessian bound.
Let ι and κ be finite index types. Let B be a real positive semidefinite matrix on ι, and let Tₐ be a family of symmetric real matrices indexed by κ. Define the κ-by-κ matrix
Then G is positive semidefinite.
The result provides a trace-weighted Gram-matrix formulation useful for controlling families of symmetric derivative matrices.
Formalization Note The statement is purely finite-dimensional and algebraic; it does not itself assert the probabilistic expectation inequality reviewed for the cited paper item.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.
theorem traceGram_posSemidef {ι κ : Type*} [Fintype ι] [Fintype κ]
(B : Matrix ι ι ℝ) (hB : B.PosSemidef)
(T : κ → Matrix ι ι ℝ) (hT : ∀ a, (T a).IsSymm) :
(Matrix.of fun a b => (B * T a * B * T b).trace).PosSemidef
Module navigation
Module: Analysis/Matrix/Positivity.
Supporting theorems: posSemidef_weightedGram.
Previous: trace_mul_nonneg · Next: trace_forcing_add_twice_energy_nonneg.
Source excerpt, lines 386–389 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Positivity
theorem FunctionalInequalities.Analysis.traceGram_posSemidef_readable {ι κ : Type*} [Fintype ι] [Fintype κ]
(B : Matrix ι ι ℝ) (hB : B.PosSemidef)
(T : κ → Matrix ι ι ℝ) (hT : ∀ a, (T a).IsSymm) :
(Matrix.of fun a b => (B * T a * B * T b).trace).PosSemidef := by sorry