Four-Tensor Trace Energy Comparison

This formalizes a finite-dimensional trace-energy comparison used in Theorem 2.5 of Letwin (arXiv:2607.24164v1), cited there as the key moment-map Hessian bound.

Let n be a natural number. Let B and W be real positive semidefinite n-by-n matrices, let H be positive definite, and let T(a,b,c) be a real three-tensor satisfying

1. T(a,b,c)=T(b,a,c) for all a,b,c;
2. T(a,b,c)=T(a,c,b) for all a,b,c.

For Tᵢ with entries T(i,a,b), define

$$D=\sum_{i,j}(H^{-1})_{ij}\operatorname{tr}(B T_i B T_j),$$

and let G be the matrix with entries $G_{ij}=\operatorname{tr}(H^{-1}T_iH^{-1}T_j)$. Then

$$0\leq D,$$

and

$$4D\leq 2\operatorname{tr}\!\bigl(BHB(-H+HWH+G)\bigr)+2D+2\operatorname{tr}(BHBH).$$

This is a technical pointwise comparison for the tensor energy and weak trace density, valid in every finite dimension, including the possibility that B is singular.

Formalization Note Matrix inverse is the Lean inverse of the positive-definite matrix H, and all sums and traces are over Fin n.

Original Lean declaration header

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

theorem four_tensor_trace_le_density_add_twice_energy {n : ℕ}
    (B H W : Matrix (Fin n) (Fin n) ℝ)
    (hB : B.PosSemidef) (hH : H.PosDef) (hW : W.PosSemidef)
    (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) :
    let Tm := fun i => Matrix.of fun a b => T i a b
    let G := Matrix.of fun i j => (H⁻¹ * Tm i * H⁻¹ * Tm j).trace
    let D := ∑ i : Fin n, ∑ j : Fin n, H⁻¹ i j * (B * Tm i * B * Tm j).trace
    0 ≤ D ∧ 4 * D ≤
      (2 * (B * H * B * (-H + H * W * H + G)).trace + 2 * D) +
        2 * (B * H * B * H).trace

Module navigation

Module: Analysis/Matrix/TraceGram.

Supporting theorems: letwin_tensor_comparison_trace_gram, traceGram_posSemidef, trace_mul_nonneg.

Previous: letwin_tensor_comparison_trace_gram.

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

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_TraceGram

theorem FunctionalInequalities.Analysis.four_tensor_trace_le_density_add_twice_energy_readable {n : ℕ}
    (B H W : Matrix (Fin n) (Fin n) ℝ)
    (hB : B.PosSemidef) (hH : H.PosDef) (hW : W.PosSemidef)
    (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) :
    let Tm := fun i => Matrix.of fun a b => T i a b
    let G := Matrix.of fun i j => (H⁻¹ * Tm i * H⁻¹ * Tm j).trace
    let D := ∑ i : Fin n, ∑ j : Fin n, H⁻¹ i j * (B * Tm i * B * Tm j).trace
    0 ≤ D ∧ 4 * D ≤
      (2 * (B * H * B * (-H + H * W * H + G)).trace + 2 * D) +
        2 * (B * H * B * H).trace := by sorry