Nonnegative Trace Forcing Expression

Proved

FunctionalInequalities.Analysis.trace_forcing_add_twice_energy_nonneg_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes a pointwise trace positivity expression associated with Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $n\in\mathbb N$ , let $B,H,R,W$ be real matrices on $\operatorname{Fin}(n)$ , and let $T_i$ be a family of such matrices indexed by $i\in\operatorname{Fin}(n)$ . Assume that $B,H,R,W$ are positive semidefinite and every $T_i$ is symmetric. Define the trace Gram matrix $G_R$ by

(G_R)_{ij}=\operatorname{tr}(RT_iRT_j).

Then

\begin{aligned} 0\le{}&2\operatorname{tr}\!\bigl(BHB(-H+HWH+G_R)\bigr)\\ &+2\sum_{i,j}R_{ij}\operatorname{tr}(BT_iBT_j) +2\operatorname{tr}(BHBH). \end{aligned}

This is a technical matrix inequality combining positive-semidefinite trace pairings and a trace Gram matrix.

Formalization Note The sums range over Fin n, and the statement includes $n=0$ .

Original Lean declaration header

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

theorem trace_forcing_add_twice_energy_nonneg {n : ℕ}
    (B H R W : Matrix (Fin n) (Fin n) ℝ)
    (hB : B.PosSemidef) (hH : H.PosSemidef) (hR : R.PosSemidef) (hW : W.PosSemidef)
    (T : Fin n → Matrix (Fin n) (Fin n) ℝ) (hT : ∀ i : Fin n, (T i).IsSymm) :
    0 ≤ (2 * (B * H * B * (-H + H * W * H +
        (Matrix.of fun i j => (R * T i * R * T j).trace))).trace +
      2 * ∑ i : Fin n, ∑ j : Fin n, R i j * (B * T i * B * T j).trace) +
      2 * (B * H * B * H).trace

Module navigation

Module: Analysis/Matrix/Positivity.

Supporting theorems: traceGram_posSemidef, trace_mul_nonneg.

Previous: traceGram_posSemidef.

Source excerpt, lines 464–471 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Positivity

Formal statement


theorem FunctionalInequalities.Analysis.trace_forcing_add_twice_energy_nonneg_readable {n : ℕ}
    (B H R W : Matrix (Fin n) (Fin n) ℝ)
    (hB : B.PosSemidef) (hH : H.PosSemidef) (hR : R.PosSemidef) (hW : W.PosSemidef)
    (T : Fin n → Matrix (Fin n) (Fin n) ℝ) (hT : ∀ i : Fin n, (T i).IsSymm) :
    0 ≤ (2 * (B * H * B * (-H + H * W * H +
        (Matrix.of fun i j => (R * T i * R * T j).trace))).trace +
      2 * ∑ i : Fin n, ∑ j : Fin n, R i j * (B * T i * B * T j).trace) +
      2 * (B * H * B * H).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#L461-L489 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.Positivity`, declaration `FunctionalInequalities.Analysis.trace_forcing_add_twice_energy_nonneg`; the repository is private at upload time).

View graph