Prove2Me

Permutation Fiber Cardinality

Proved
FunctionalInequalities.Analysis.Tensor.card_filter_perm_apply_last_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement counts permutations with a prescribed image of the last index.

For d∈Nd\in\mathbb N and k∈Fin⁡(d+1)k\in\operatorname{Fin}(d+1), consider permutations σ\sigma of Fin⁡(d+1)\operatorname{Fin}(d+1) satisfying σ(last⁡(d))=k\sigma(\operatorname{last}(d))=k. Their number is exactly d!d!:

#{σ∈Sym⁡(Fin⁡(d+1)):σ(last⁡(d))=k}=d!.\#\{\sigma\in\operatorname{Sym}(\operatorname{Fin}(d+1)):\sigma(\operatorname{last}(d))=k\}=d!.

This is a finite combinatorial identity used to group permutation sums according to the value of their last argument.

Original Lean declaration header

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

theorem card_filter_perm_apply_last_eq {d : ℕ} (k : Fin (d + 1)) :
    (Finset.univ.filter fun σ : Equiv.Perm (Fin (d + 1)) => σ (Fin.last d) = k).card =
      d.factorial

Module navigation

Module: Analysis/Tensor/Multilinear.

Next: exists_perm_init_comp_eq.

Source excerpt, lines 85–87 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Tensor_Multilinear
Formal statement

theorem FunctionalInequalities.Analysis.Tensor.card_filter_perm_apply_last_eq_readable {d : ℕ} (k : Fin (d + 1)) :
    (Finset.univ.filter fun σ : Equiv.Perm (Fin (d + 1)) => σ (Fin.last d) = k).card =
      d.factorial := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Tensor/Multilinear.lean#L84-L132 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Tensor.Multilinear`, declaration `FunctionalInequalities.Analysis.Tensor.card_filter_perm_apply_last_eq`; the repository is private at upload time).

View graph