One-Slot Delta Collapse With Two Tensors

Proved

FunctionalInequalities.Analysis.CoordinateTensor.slot_sum_two_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This auxiliary lemma evaluates a two-tensor coordinate sum with delta constraints.

For coordinate tensors $S,T$ , a real matrix $M$ , and order $r$ and dimension $n$ , the sum

\sum_{J,K}S_JT_K\sum_s \left(\prod_{u\ne s}\delta_{J_u,K_u}\right)(-M_{J_sK_s})

is equal to

-\langle S,\Sigma_M T\rangle.

Here $\Sigma_M T=\sum_sM^{(s)}T$ . The lemma is an internal algebraic component of the energy-form derivative calculation.

Original Lean declaration header

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

private lemma slot_sum_two
    (S T : (Fin r → Fin n) → ℝ) (M : Matrix (Fin n) (Fin n) ℝ) :
    (∑ J : Fin r → Fin n, ∑ K : Fin r → Fin n,
      S J * T K * (∑ s : Fin r,
        (∏ u ∈ Finset.univ.erase s, if J u = K u then (1 : ℝ) else 0) *
          (-M (J s) (K s)))) =
      -inner S (actSum M T)

Module navigation

Module: Analysis/Tensor/EnergyForm.

Definition modules: Analysis/Tensor/SlotAction.

Supporting theorems: sum_mul_prod_delta_erase.

Previous: fderiv_fderiv_apply_eq_deriv_deriv_line · Next: two_slot_sum.

Source excerpt, lines 679–685 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_EnergyForm

variable {n r : ℕ}

Formal statement


 lemma FunctionalInequalities.Analysis.CoordinateTensor.slot_sum_two_readable
    (S T : (Fin r → Fin n) → ℝ) (M : Matrix (Fin n) (Fin n) ℝ) :
    (∑ J : Fin r → Fin n, ∑ K : Fin r → Fin n,
      S J * T K * (∑ s : Fin r,
        (∏ u ∈ Finset.univ.erase s, if J u = K u then (1 : ℝ) else 0) *
          (-M (J s) (K s)))) =
      -inner S (actSum M T) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Tensor/EnergyForm.lean#L678-L736 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Tensor.EnergyForm`, declaration `_private.FunctionalInequalities.Analysis.Tensor.EnergyForm.0.FunctionalInequalities.Analysis.CoordinateTensor.slot_sum_two`; the repository is private at upload time).

View graph