Prove2Me

Jordan Trace Energy Domination

Proved
FunctionalInequalities.Analysis.jordan_trace_domination_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This statement gives trace-energy domination arising from a Jordan decomposition.

Let ι be a finite index type with decidable equality. Let P and N be positive semidefinite real matrices, and let H be symmetric. Then

tr⁡((P−N)H(P−N)H)≤tr⁡(PHPH)+tr⁡(NHNH).\operatorname{tr}\bigl((P-N)H(P-N)H\bigr) \leq \operatorname{tr}(PHPH)+\operatorname{tr}(NHNH).

No commutation between the matrices is assumed.

This pointwise matrix inequality is useful for extending estimates from positive semidefinite weights to arbitrary symmetric weights.

Formalization Note The result is purely finite-dimensional and uses ordinary real matrix multiplication and trace.

Original Lean declaration header

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

theorem jordan_trace_domination {P N H : Matrix ι ι ℝ}
    (hP : P.PosSemidef) (hN : N.PosSemidef) (hH : H.IsSymm) :
    ((P - N) * H * (P - N) * H).trace ≤
      (P * H * P * H).trace + (N * H * N * H).trace

Module navigation

Module: Analysis/Matrix/Trace/Energy.

Previous: trace_energy_nonneg · Next: letwin_trace_weighted_slices.

Source excerpt, lines 117–120 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Trace_Energy

variable {ι : Type*} [Fintype ι] [DecidableEq ι]
Formal statement

theorem FunctionalInequalities.Analysis.jordan_trace_domination_readable {P N H : Matrix ι ι ℝ}
    (hP : P.PosSemidef) (hN : N.PosSemidef) (hH : H.IsSymm) :
    ((P - N) * H * (P - N) * H).trace ≤
      (P * H * P * H).trace + (N * H * N * 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/Trace/Energy.lean#L115-L137 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.Trace.Energy`, declaration `FunctionalInequalities.Analysis.jordan_trace_domination`; the repository is private at upload time).

View graph