Two-Slot Delta Collapse

Proved

FunctionalInequalities.Analysis.CoordinateTensor.sum_mul_prod_delta_erase_erase_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement evaluates delta constraints leaving two tensor slots free.

Let $J:\operatorname{Fin}(r)\to\operatorname{Fin}(n)$ , let distinct slots $s,t\in\operatorname{Fin}(r)$ satisfy $s\ne t$ , and let $f$ be real-valued on coordinate tensors. Then

\sum_{J'}f(J')\prod_{u\notin\{s,t\}}\delta_{J_u,J'_u} =\sum_{k,l\in\operatorname{Fin}(n)}f(J[s\mapsto k][t\mapsto l]).

The identity is a finite reindexing tool for sums with all coordinates fixed except two.

Original Lean declaration header

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

theorem sum_mul_prod_delta_erase_erase (J : Fin r → Fin n) {s t : Fin r} (hst : s ≠ t)
    (f : (Fin r → Fin n) → ℝ) :
    ∑ J' : Fin r → Fin n, f J' *
        ∏ s' ∈ (Finset.univ.erase s).erase t, (if J s' = J' s' then (1 : ℝ) else 0) =
      ∑ k, ∑ l, f (Function.update (Function.update J s k) t l)

Module navigation

Module: Analysis/Tensor/EnergyForm.

Previous: hasDerivAt_energyForm_line · Next: fderiv_fderiv_apply_eq_deriv_deriv_line.

Source excerpt, lines 496–500 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_EnergyForm

variable {n r : ℕ}

Formal statement


theorem FunctionalInequalities.Analysis.CoordinateTensor.sum_mul_prod_delta_erase_erase_readable (J : Fin r → Fin n) {s t : Fin r} (hst : s ≠ t)
    (f : (Fin r → Fin n) → ℝ) :
    ∑ J' : Fin r → Fin n, f J' *
        ∏ s' ∈ (Finset.univ.erase s).erase t, (if J s' = J' s' then (1 : ℝ) else 0) =
      ∑ k, ∑ l, f (Function.update (Function.update J s k) t l) := by sorry

Source

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

View graph