An expander family exists

The three strands meet here. ExpanderRandom produces, for every n, thirty permutations of Fin n no vertex set of at most half the vertices survives; PermGraph turns those into a 60-regular graph with edge expansion 1/600; and Cheeger converts edge expansion into a spectral gap once enough self-loops are added to make the walk lazy. Relabelling the resulting 120 darts as Fin 120 puts the graph in the rotation-map form ExpanderFamily asks for.

The construction is not explicit — the permutations come from Classical.choose on a counting argument — which is all the mathematics of Dinur's proof needs. An explicit family would be needed only to make the reduction itself polynomial-time computable.

Main definitions

• Complexity.goodPerms — the chosen permutations
• Complexity.randExpander — the resulting ExpanderFamily

noncomputable def Complexity.goodPerms (n : ℕ) : Fin 30 → Equiv.Perm (Fin n)

Thirty permutations of Fin n that expand every small set.

Equations

• Complexity.goodPerms n = Classical.choose ⋯

theorem Complexity.goodPerms_spec (n : ℕ) (S : Finset (Fin n)) (hS : 2 * S.card ≤ n) : ∃ (i : Fin 30), S.card ≤ 10 * escape (goodPerms n i) S

noncomputable def Complexity.baseGraph (n : ℕ) : RegGraph

The 60-regular graph of those permutations.

Equations

• Complexity.baseGraph n = Complexity.RegGraph.permsGraph Complexity.baseGraph._proof_1 (Complexity.goodPerms n)

theorem Complexity.edgeExpansion_baseGraph (n : ℕ) : (baseGraph n).EdgeExpansion (1 / (2 * 10 * 30))

theorem Complexity.deg_baseGraph (n : ℕ) : (baseGraph n).deg = 60

noncomputable def Complexity.lazyGraph (n : ℕ) : RegGraph

The lazy walk on it: a self-loop for every dart.

Equations

• Complexity.lazyGraph n = (Complexity.baseGraph n).padLoops (Complexity.baseGraph n).deg

noncomputable def Complexity.randLam : ℝ

The spectral bound the construction achieves.

Equations

• Complexity.randLam = 1 - (1 / (2 * 10 * 30)) ^ 2 / 4

theorem Complexity.randLam_nonneg : 0 ≤ randLam

theorem Complexity.randLam_lt_one : randLam < 1

theorem Complexity.spectral_lazyGraph (n : ℕ) : (lazyGraph n).SpectralBound randLam

theorem Complexity.deg_lazyGraph (n : ℕ) : (lazyGraph n).deg = 120

theorem Complexity.card_lazyDarts (n : ℕ) : Fintype.card (lazyGraph n).D = 120

noncomputable def Complexity.dartEquiv (n : ℕ) : (lazyGraph n).D ≃ Fin 120

The darts of the lazy graph, named by Fin 120.

Equations

• Complexity.dartEquiv n = Fintype.equivFinOfCardEq ⋯

noncomputable def Complexity.randGraph (n : ℕ) : RegGraph

The graph on n vertices with Fin 120 darts.

Equations

• Complexity.randGraph n = (Complexity.lazyGraph n).relabel (Complexity.dartEquiv n)

theorem Complexity.spectral_randGraph (n : ℕ) : (randGraph n).SpectralBound randLam

noncomputable def Complexity.randRot (n : ℕ) : Fin n × Fin 120 → Fin n × Fin 120

Its rotation map, as data on Fin n × Fin 120.

Equations

• Complexity.randRot n = (Complexity.randGraph n).rot

theorem Complexity.randRot_involutive (n : ℕ) : Function.Involutive (randRot n)

theorem Complexity.ofRot_randRot (n : ℕ) : RegGraph.ofRot 120 ofRot_randRot._proof_1 n (randRot n) ⋯ = randGraph n

noncomputable def Complexity.randExpander : ExpanderFamily

An expander family.

Equations

• One or more equations did not get rendered due to their size.