Counting permutations that keep a set inside a set

The expander existence proof needs one combinatorial estimate: of the n! permutations of Fin n, at most descFactorial s k · (n - k)! map a given k-element set inside a given s-element set.

The proof is the obvious one, made precise. Restricting a permutation to K gives an injection into S; there are descFactorial s k of those. Two permutations with the same restriction differ only outside K, where they are injections from an (n - k)-set into the complement of the common image — another (n - k)-set — so each restriction is shared by at most (n - k)! permutations.

Main results

• Complexity.card_perm_mapsTo_le — the estimate
• Complexity.card_perm_escape_le — its consequence for the escape count: few permutations move only a small part of S out of S

noncomputable def Complexity.escape {n : ℕ} (σ : Equiv.Perm (Fin n)) (S : Finset (Fin n)) : ℕ

How many points of S the permutation σ sends outside S.

Equations

• Complexity.escape σ S = {v ∈ S | σ v ∉ S}.card

Restrictions of a permutation

noncomputable def Complexity.permsInto {n : ℕ} (S K : Finset (Fin n)) : Finset (Equiv.Perm (Fin n))

The permutations mapping K into S.

Equations

• Complexity.permsInto S K = {σ : Equiv.Perm (Fin n) | ∀ v ∈ K, σ v ∈ S}

noncomputable def Complexity.restrs {n : ℕ} (S K : Finset (Fin n)) : Finset (↥K → Fin n)

The restrictions that can occur: injective maps of K into S.

Equations

• Complexity.restrs S K = {f : ↥K → Fin n | Function.Injective f ∧ ∀ (v : ↥K), f v ∈ S}

theorem Complexity.mem_restrs {n : ℕ} {S K : Finset (Fin n)} {f : ↥K → Fin n} (hf : f ∈ restrs S K) : Function.Injective f ∧ ∀ (v : ↥K), f v ∈ S

theorem Complexity.card_restrs_le {n : ℕ} (S K : Finset (Fin n)) : (restrs S K).card ≤ S.card.descFactorial K.card

There are few restrictions.

noncomputable def Complexity.restrImage {n : ℕ} {K : Finset (Fin n)} (f : ↥K → Fin n) : Finset (Fin n)

The values of a restriction.

Equations

• Complexity.restrImage f = Finset.image f Finset.univ

theorem Complexity.card_restrImage {n : ℕ} {S K : Finset (Fin n)} {f : ↥K → Fin n} (hf : f ∈ restrs S K) : (restrImage f).card = K.card

theorem Complexity.card_fiber_le {n : ℕ} (S K : Finset (Fin n)) (f : ↥K → Fin n) (hf : f ∈ restrs S K) : {σ ∈ permsInto S K | (fun (v : ↥K) => σ ↑v) = f}.card ≤ (n - K.card).factorial

Each restriction is shared by few permutations.

theorem Complexity.card_perm_mapsTo_le {n : ℕ} (S K : Finset (Fin n)) : (permsInto S K).card ≤ S.card.descFactorial K.card * (n - K.card).factorial

The estimate.

Permutations with little escape

theorem Complexity.card_perm_escape_le {n : ℕ} (S : Finset (Fin n)) (t : ℕ) : {σ : Equiv.Perm (Fin n) | escape σ S ≤ t}.card ≤ S.card.choose (S.card - t) * (S.card.descFactorial (S.card - t) * (n - (S.card - t)).factorial)

Few permutations move only a little of S out of S. Such a permutation keeps a (s - t)-element subset of S inside S, and there are few subsets and, by card_perm_mapsTo_le, few permutations for each.