Positive Semidefinite Weighted Gram Matrix
ProvedFunctionalInequalities.Analysis.posSemidef_weightedGram_readableThis statement establishes positivity of a weighted Gram matrix.
Let ι and κ be finite index types, let A be a real matrix on ι, and assume A is positive semidefinite. For an arbitrary family of real matrices Tᵢ indexed by κ, define G by
Then G is positive semidefinite. Equivalently, this is the matrix representation of F(A ⊗ A)Fᵀ, where F records the entries of the matrices Tᵢ.
This is a reusable finite-dimensional Gram-matrix construction for tensor and trace-energy estimates.
Formalization Note The matrix Matrix.PosSemidef and all sums range over finite types; no symmetry or definiteness beyond positive semidefiniteness of A is assumed.
Original Lean declaration header
Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.
theorem posSemidef_weightedGram (A : Matrix ι ι ℝ) (hA : A.PosSemidef)
(T : κ → Matrix ι ι ℝ) :
(Matrix.of fun i j => ∑ a, ∑ b, ∑ c, ∑ d,
A a c * A b d * T i a b * T j c d).PosSemidef
Module navigation
Module: Analysis/Matrix/Positivity.
Next: exists_quadraticFloor_of_posDef.
Source excerpt, lines 47–50 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Positivity
variable {ι κ : Type*} [Fintype ι] [Fintype κ]
theorem FunctionalInequalities.Analysis.posSemidef_weightedGram_readable (A : Matrix ι ι ℝ) (hA : A.PosSemidef)
(T : κ → Matrix ι ι ℝ) :
(Matrix.of fun i j => ∑ a, ∑ b, ∑ c, ∑ d,
A a c * A b d * T i a b * T j c d).PosSemidef := by sorry