Families of expanders

A family of expanders (Cslib.RotationMap.ExpanderFamily) bundles a choice of a D-regular multigraph on every finite type with a common bound μ on their spectral expansions; constructions that need expanders of constant degree on arbitrary vertex sets, such as Dinur's preprocessing Dinur, Section 3.1, take one as a parameter. The notion is defined apart from the non-constructive family Cslib.RotationMap.expanderFamily, so that explicit families do not depend on it.

Main definitions

• Cslib.RotationMap.ExpanderFamily: a family of D-regular multigraphs on all finite types with spectral expansion at most μ.
• Cslib.RotationMap.ExpanderFamily.ofFin: interpret an indexed family on arbitrary finite types.

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

structure Cslib.RotationMap.ExpanderFamily (D : Type u_1) [Fintype D] (μ : ℝ) : Type (max (u + 1) u_1)

A family of expanders of degree |D| and spectral bound μ: a D-regular multigraph on every finite type V in the universe u, of spectral expansion at most μ. It is a family of expanders in the usual sense when D is finite and nonempty and μ < 1.

• graph (V : Type u) [Fintype V] : RotationMap V D

  The multigraph on a finite type.

• spectralExpansion_graph_le (V : Type u) [Fintype V] : (self.graph V).spectralExpansion ≤ μ

  The spectral expansion of each multigraph of the family is at most μ.

noncomputable def Cslib.RotationMap.ExpanderFamily.ofFin {D : Type u_1} [Fintype D] {μ : ℝ} (graph : (n : ℕ) → RotationMap (Fin n) D) (bound : ∀ (n : ℕ), (graph n).spectralExpansion ≤ μ) : ExpanderFamily D μ

Interpret an indexed family on arbitrary finite types by choosing a numbering. Only this mathematical wrapper is noncomputable; executable clients should use the original indexed family or supply their own vertex equivalence to RotationMap.reindex.