Equal Fiber Cardinalities for Block Images

This is a finite-combinatorial fiber-counting lemma.

Let $\Omega$ be finite and let $A,Q,F,F'\subseteq\Omega$ be finite subsets. Assume that $F$ and $F'$ are both $|A|$-element subsets of $Q$. Then the two fibers of the map $\sigma\mapsto\sigma(A)$, restricted to permutations fixing every point outside $Q$, have equal cardinality:

This uniformity is used when grouping permutation sums by the image of $A$.

Original Lean declaration header

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

theorem card_fiber_eq {A Q : Finset Ω} {F F' : Finset Ω}
    (hF : F ∈ Q.powersetCard A.card) (hF' : F' ∈ Q.powersetCard A.card) :
    ((fixingOutside Q).filter fun σ : Equiv.Perm Ω => A.image σ = F).card =
      ((fixingOutside Q).filter fun σ : Equiv.Perm Ω => A.image σ = F').card

Module navigation

Module: Analysis/Tensor/Symmetrization.

Supporting theorems: exists_mem_fixingOutside_image_eq.

Previous: image_mem_powersetCard_of_mem_fixingOutside · Next: sum_fixingOutside_eq_smul_sum.

Source excerpt, lines 771–774 · Frozen source 408915f.