Letwin Tensor Comparison in Trace-Gram Form

This formalizes equation (2.12) of Letwin (arXiv:2607.24164v1), locator (2.12), p. 10, in trace-Gram coordinates.

Let $H$ be positive definite, $B$ Hermitian, and let $T_{abc}$ have the two symmetries $T_{abc}=T_{bac}$ and $T_{abc}=T_{acb}$. Define the trace-Gram matrix

Then

This coordinate form is reusable when the Gram forcing is represented as a matrix trace rather than as an expanded fourfold sum.

Original Lean declaration header

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

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

Module navigation

Module: Analysis/Matrix/TraceGram.

Supporting theorems: letwin_tensor_comparison, trace_mul_mul_mul_eq_sum.

Next: four_tensor_trace_le_density_add_twice_energy.

Source excerpt, lines 50–58 · Frozen source 408915f.