Nonnegativity of Weighted Trace Energy

This formalizes the nonnegativity of a weighted trace energy and is cited partially by Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $B$ and $H$ be real matrices on a finite index type $\iota$. Assume that $B$ is symmetric and that $H$ is positive semidefinite. Then

Here $\operatorname{tr}$ is the matrix trace and juxtaposition denotes matrix multiplication.

The result provides the pointwise positivity input for matrix-field trace estimates, without requiring $B$ itself to be positive semidefinite.

Formalization Note The finite index type may be empty, and no commutation assumption on $B$ and $H$ is present.

Original Lean declaration header

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

theorem trace_energy_nonneg {B H : Matrix ι ι ℝ}
    (hB : B.IsSymm) (hH : H.PosSemidef) :
    0 ≤ (B * H * B * H).trace

Module navigation

Module: Analysis/Matrix/Trace/Energy.

Next: jordan_trace_domination.

Source excerpt, lines 87–89 · Frozen source 408915f.