Permutation of Entries After Removing One Index

Proved

FunctionalInequalities.Analysis.Tensor.exists_perm_init_comp_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement describes the first $d$ entries of a permuted $(d+1)$ -tuple.

Let $\alpha$ be a type, let $h:\operatorname{Fin}(d+1)\to\alpha$ , let $\sigma$ be a permutation of $\operatorname{Fin}(d+1)$ , and let $k\in\operatorname{Fin}(d+1)$ . If

\sigma(\operatorname{last}(d))=k,

then there exists a permutation $\tau$ of $\operatorname{Fin}(d)$ such that

\operatorname{init}(h\circ\sigma)=\operatorname{removeNth}(k,h)\circ\tau.

Thus, after the entry indexed by $k$ is removed, the remaining entries agree up to permutation. This technical lemma supports reorganizing symmetrized multilinear expressions.

Original Lean declaration header

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

theorem exists_perm_init_comp_eq {α : Type*} {d : ℕ} (h : Fin (d + 1) → α)
    (σ : Equiv.Perm (Fin (d + 1))) {k : Fin (d + 1)} (hk : σ (Fin.last d) = k) :
    ∃ τ : Equiv.Perm (Fin d), Fin.init (h ∘ σ) = k.removeNth h ∘ τ

Module navigation

Module: Analysis/Tensor/Multilinear.

Previous: card_filter_perm_apply_last_eq · Next: sum_perm_inner_init_last.

Source excerpt, lines 135–137 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Multilinear

Formal statement


theorem FunctionalInequalities.Analysis.Tensor.exists_perm_init_comp_eq_readable {α : Type*} {d : ℕ} (h : Fin (d + 1) → α)
    (σ : Equiv.Perm (Fin (d + 1))) {k : Fin (d + 1)} (hk : σ (Fin.last d) = k) :
    ∃ τ : Equiv.Perm (Fin d), Fin.init (h ∘ σ) = k.removeNth h ∘ τ := by sorry

Source

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

View graph