Permutation Sum for a Symmetric Multilinear Map

Proved

FunctionalInequalities.Analysis.Tensor.sum_perm_inner_init_last_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement evaluates a permutation sum for a symmetric continuous multilinear map.

Let $E$ be a real inner-product space, let $d\in\mathbb N$ , and let $\Phi:E^d\to E$ be a continuous $d$ -linear map satisfying

\Phi(v\circ\tau)=\Phi(v)

for every permutation $\tau$ of $\operatorname{Fin}(d)$ and every $v:\operatorname{Fin}(d)\to E$ . For $h:\operatorname{Fin}(d+1)\to E$ , one has

\sum_{\sigma\in\operatorname{Sym}(d+1)} \left\langle \Phi\bigl(\operatorname{init}(h\circ\sigma)\bigr), h(\sigma(\operatorname{last}(d))) \right\rangle =(d!)\sum_{k\in\operatorname{Fin}(d+1)} \left\langle \Phi(\operatorname{removeNth}(k,h)),h(k) \right\rangle.

This is the counting identity underlying symmetrization of a multilinear map paired with one additional vector.

Original Lean declaration header

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

theorem sum_perm_inner_init_last {d : ℕ} (Φ : ContinuousMultilinearMap ℝ (fun _ : Fin d => E) E)
    (hΦ : ∀ (τ : Equiv.Perm (Fin d)) (v : Fin d → E), Φ (v ∘ τ) = Φ v) (h : Fin (d + 1) → E) :
    ∑ σ : Equiv.Perm (Fin (d + 1)), ⟪Φ (Fin.init (h ∘ σ)), h (σ (Fin.last d))⟫ =
      (d.factorial : ℝ) * ∑ k : Fin (d + 1), ⟪Φ (k.removeNth h), h k⟫

Module navigation

Module: Analysis/Tensor/Multilinear.

Supporting theorems: card_filter_perm_apply_last_eq, exists_perm_init_comp_eq.

Previous: exists_perm_init_comp_eq.

Source excerpt, lines 166–169 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Multilinear

open scoped RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.Tensor.sum_perm_inner_init_last_readable {d : ℕ} (Φ : ContinuousMultilinearMap ℝ (fun _ : Fin d => E) E)
    (hΦ : ∀ (τ : Equiv.Perm (Fin d)) (v : Fin d → E), Φ (v ∘ τ) = Φ v) (h : Fin (d + 1) → E) :
    ∑ σ : Equiv.Perm (Fin (d + 1)), ⟪Φ (Fin.init (h ∘ σ)), h (σ (Fin.last d))⟫ =
      (d.factorial : ℝ) * ∑ k : Fin (d + 1), ⟪Φ (k.removeNth h), h k⟫ := by sorry

Source

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

View graph