One-Slot Delta Collapse

Proved

FunctionalInequalities.Analysis.CoordinateTensor.sum_mul_prod_delta_erase_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement evaluates a finite sum constrained by Kronecker-delta factors.

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

\sum_{J'}f(J')\prod_{s'\ne s}\delta_{J_{s'},J'_{s'}} =\sum_{k\in\operatorname{Fin}(n)}f(J[s\mapsto k]).

The product forces $J'$ to agree with $J$ outside slot $s$ , leaving only the value in slot $s$ free. This finite combinatorial identity is used to collapse coordinate sums.

Original Lean declaration header

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

theorem sum_mul_prod_delta_erase (J : Fin r → Fin n) (s : Fin r) (f : (Fin r → Fin n) → ℝ) :
    ∑ J' : Fin r → Fin n, f J' * ∏ s' ∈ Finset.univ.erase s, (if J s' = J' s' then (1 : ℝ) else 0) =
      ∑ k, f (Function.update J s k)

Module navigation

Module: Analysis/Tensor/EnergyForm.

Previous: contDiffAt_energyForm · Next: slot_derivative_sum.

Source excerpt, lines 95–97 · 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_readable (J : Fin r → Fin n) (s : Fin r) (f : (Fin r → Fin n) → ℝ) :
    ∑ J' : Fin r → Fin n, f J' * ∏ s' ∈ Finset.univ.erase s, (if J s' = J' s' then (1 : ℝ) else 0) =
      ∑ k, f (Function.update J s k) := by sorry

Source

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

View graph