A tuple of permutations that expands

The counting argument. Of the (n!)^30 tuples of thirty permutations of Fin n, not all can fail to expand: a tuple fails at a vertex set S of at most half the vertices exactly when every one of its thirty permutations keeps all but a tenth of S inside S. PermCount bounds how many permutations do that for a fixed S; PermArith.key_estimate turns the thirtieth power of that bound into (n!)^30 / 2^{|S|}, with room to spare for the C(n,s) sets of each size; and summing 2^{-s} over s ≥ 1 stays below one.

Everything is done with natural numbers — the geometric series appears as an induction that carries the slack + K explicitly, so no division is needed.

Main definitions

• Complexity.escLE — the permutations keeping all but t points of S in S
• Complexity.tOf — the escape a set of a given size is allowed

Main results

• Complexity.exists_good_perms — a tuple of thirty permutations for which every set of at most half the vertices is moved out of itself, by at least a tenth of it, by one of them

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

The permutations moving at most t points of S out of S.

Equations

• Complexity.escLE S t = {σ : Equiv.Perm (Fin n) | Complexity.escape σ S ≤ t}

def Complexity.tOf {n : ℕ} (S : Finset (Fin n)) : ℕ

The escape a set of size s is allowed before it counts as expanding.

Equations

• Complexity.tOf S = (S.card - 1) / 10

theorem Complexity.ten_mul_tOf_le {n : ℕ} (S : Finset (Fin n)) : 10 * tOf S ≤ S.card

theorem Complexity.mem_escLE_iff {n : ℕ} {S : Finset (Fin n)} {σ : Equiv.Perm (Fin n)} (hS : 1 ≤ S.card) : σ ∈ escLE S (tOf S) ↔ ¬S.card ≤ 10 * escape σ S

def Complexity.escB (n s : ℕ) : ℕ

The bound on how many permutations fail to expand a set of size s.

Equations

• Complexity.escB n s = s.choose ((s - 1) / 10) * s.descFactorial (s - (s - 1) / 10) * (n - (s - (s - 1) / 10)).factorial

theorem Complexity.card_escLE_le {n : ℕ} (S : Finset (Fin n)) : (escLE S (tOf S)).card ≤ escB n S.card

theorem Complexity.two_pow_mul_escB_le {n s : ℕ} (hs : 1 ≤ s) (hsn : 2 * s ≤ n) : 2 ^ s * (n.choose s * escB n s ^ 30) ≤ n.factorial ^ 30

The per-size estimate.

The geometric slack

The union bound

theorem Complexity.exists_good_perms (n : ℕ) : ∃ (σ : Fin 30 → Equiv.Perm (Fin n)), ∀ (S : Finset (Fin n)), 2 * S.card ≤ n → S.Nonempty → ∃ (i : Fin 30), S.card ≤ 10 * escape (σ i) S

A tuple that expands.