Constant-degree expanders exist

Every finite type V carries a 120-regular multigraph of spectral expansion at most 1 - 1 / 360000 (exists_spectralExpansion_le): constant-degree expanders exist on any number of vertices, with a degree and a spectral bound that do not depend on that number (exists_forall_exists_spectralExpansion_le). The proof combines three ingredients.

• Thirty permutations of V move a tenth of every set of at most half of the vertices out of it (Cslib.exists_perms_card_le_mul_card_filter_notMem, a counting argument).
• Their 60-regular multigraph Cslib.RotationMap.ofPerms therefore has edge expansion at least 1 / 5 (Cslib.RotationMap.le_edgeExpansion_ofPerms).
• Cheeger's inequality turns edge expansion into a spectral bound for its lazy graph, of degree 120 (Cslib.RotationMap.spectralExpansion_lazy_le_of_mul_card_le_card_interedges_compl).

The construction is not explicit, since the permutations come from a counting argument, and neither is the multigraph expander V chosen from it. Explicit families are built by graph products from a single expander of constant size Reingold, Vadhan and Wigderson, Section 1.2 Arora and Barak, Section 21.3.

The multigraphs expander V form a family of expanders (Cslib.RotationMap.ExpanderFamily, expanderFamily), as Dinur's preprocessing needs Dinur, Section 3.1.

Main definitions

• Cslib.RotationMap.expander: a 120-regular multigraph on V of spectral expansion at most 1 - 1 / 360000, chosen non-constructively.
• Cslib.RotationMap.expanderFamily: the family of the multigraphs expander V.

Main results

• Cslib.RotationMap.exists_spectralExpansion_le: such a multigraph exists on every finite type.
• Cslib.RotationMap.exists_forall_exists_spectralExpansion_le: constant-degree expanders exist, with the same degree and spectral bound on every finite type.
• Cslib.RotationMap.le_edgeExpansion_expander: they have edge expansion at least 1 / 6000.

References

• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders

theorem Cslib.RotationMap.exists_spectralExpansion_le (V : Type u) [Fintype V] : ∃ (G : RotationMap V (Fin 120)), G.spectralExpansion ≤ 1 - 1 / 360000

Constant-degree expanders exist Hoory, Linial and Wigderson, Theorem 4.16 Arora and Barak, Chapter 21: every finite type carries a 120-regular multigraph of spectral expansion at most 1 - 1 / 360000. It is the lazy graph of the multigraph of thirty permutations that move a tenth of every set of at most half of the vertices out of it.

theorem Cslib.RotationMap.exists_forall_exists_spectralExpansion_le : ∃ (d : ℕ), ∃ μ < 1, ∀ (V : Type u) [inst : Fintype V], ∃ (G : RotationMap V (Fin d)), G.spectralExpansion ≤ μ

Constant-degree expanders exist Hoory, Linial and Wigderson, Theorem 4.16 Arora and Barak, Chapter 21: there are a degree d and a bound μ < 1 such that every finite type carries a d-regular multigraph of spectral expansion at most μ.

theorem Cslib.RotationMap.le_edgeExpansion_of_spectralExpansion_le {V : Type u} [Fintype V] [DecidableEq V] [Nontrivial V] {G : RotationMap V (Fin 120)} (hG : G.spectralExpansion ≤ 1 - 1 / 360000) : 1 / 6000 ≤ G.edgeExpansion

A 120-regular multigraph on at least two vertices of spectral expansion at most 1 - 1 / 360000 has edge expansion at least 1 / 6000, by the easy half of Cheeger's inequality.

noncomputable def Cslib.RotationMap.expander (V : Type u) [Fintype V] : RotationMap V (Fin 120)

A 120-regular multigraph on a finite type V of spectral expansion at most 1 - 1 / 360000 (spectralExpansion_expander_le), chosen non-constructively by exists_spectralExpansion_le.

theorem Cslib.RotationMap.spectralExpansion_expander_le (V : Type u) [Fintype V] : (expander V).spectralExpansion ≤ 1 - 1 / 360000

The spectral expansion of expander V is at most 1 - 1 / 360000.

noncomputable def Cslib.RotationMap.expanderFamily : ExpanderFamily (Fin 120) (1 - 1 / 360000)

The non-explicit family of the 120-regular multigraphs expander V, of spectral expansion at most 1 - 1 / 360000.

@[simp]

theorem Cslib.RotationMap.graph_expanderFamily (V : Type u) [Fintype V] : expanderFamily.graph V = expander V

The multigraph of expanderFamily on V is expander V.

theorem Cslib.RotationMap.le_edgeExpansion_expander (V : Type u) [Fintype V] [DecidableEq V] [Nontrivial V] : 1 / 6000 ≤ (expander V).edgeExpansion

On at least two vertices, expander V has edge expansion at least 1 / 6000.