Letwin Tensor Comparison

Proved

FunctionalInequalities.Analysis.letwin_tensor_comparison_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes equation (2.12) of Letwin (arXiv:2607.24164v1), locator (2.12), p. 10.

Let $H,B$ be real $n\times n$ matrices, with $H$ positive definite and $B$ Hermitian, hence symmetric over $\mathbb R$ . Let $T_{abc}$ be a real three-tensor satisfying

T_{abc}=T_{bac}=T_{acb}

through the two stated symmetry assumptions. Write $(T_a)_{ij}=T_{aij}$ . Then

\sum_{a,b}(H^{-1})_{ab}\operatorname{tr}(BT_aBT_b) \le \sum_{i,j}(BHB)_{ij} \sum_{a,b,c,d}(H^{-1})_{ac}(H^{-1})_{bd}T_{abi}T_{cdj}.

This is the pointwise tensor comparison used in the curvature–Gram energy analysis.

Original Lean declaration header

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

theorem letwin_tensor_comparison {n : ℕ} (H B : Matrix (Fin n) (Fin n) ℝ) (hH : H.PosDef)
    (hB : B.IsHermitian) (T : Fin n → Fin n → Fin n → ℝ)
    (hT₁ : ∀ a b c, T a b c = T b a c) (hT₂ : ∀ a b c, T a b c = T a c b) :
    ∑ a, ∑ b, H⁻¹ a b * (B * Matrix.of (fun i j => T a i j) * B *
        Matrix.of (fun i j => T b i j)).trace ≤
      ∑ i, ∑ j, (B * H * B) i j *
        ∑ a, ∑ b, ∑ c, ∑ d, H⁻¹ a c * H⁻¹ b d * T a b i * T c d j

Module navigation

Module: Analysis/Matrix/Trace/Energy.

Supporting theorems: letwin_tensor_trace_identity, letwin_trace_weighted_slices.

Previous: letwin_tensor_trace_identity.

Source excerpt, lines 397–403 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Trace_Energy

Formal statement


theorem FunctionalInequalities.Analysis.letwin_tensor_comparison_readable {n : ℕ} (H B : Matrix (Fin n) (Fin n) ℝ) (hH : H.PosDef)
    (hB : B.IsHermitian) (T : Fin n → Fin n → Fin n → ℝ)
    (hT₁ : ∀ a b c, T a b c = T b a c) (hT₂ : ∀ a b c, T a b c = T a c b) :
    ∑ a, ∑ b, H⁻¹ a b * (B * Matrix.of (fun i j => T a i j) * B *
        Matrix.of (fun i j => T b i j)).trace ≤
      ∑ i, ∑ j, (B * H * B) i j *
        ∑ a, ∑ b, ∑ c, ∑ d, H⁻¹ a c * H⁻¹ b d * T a b i * T c d j := 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#L393-L449 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.Trace.Energy`, declaration `FunctionalInequalities.Analysis.letwin_tensor_comparison`; the repository is private at upload time).

View graph