Expander families, and expanderizing a graph

Dinur's preprocessing needs a fixed constant degree d and a constant lam < 1 such that every vertex count admits a d-regular graph with spectral bound lam. ExpanderFamily packages exactly that.

The family is given as raw rotation data on Fin n × Fin degree, one involution per vertex count, rather than as a function into RegGraph. That matters downstream: degree reduction puts an expander on the cloud of every vertex at once, and those clouds have different sizes, so all of them must speak the same label type Fin degree. Deriving the graphs from shared data gives that for free, and makes order and deg computations Fintype.card_fin rather than hypotheses.

Isolating the requirement this way matters for a second reason: nothing else in the development depends on how the family is built. Neither Mathlib nor this library currently contains an explicit expander construction — no spectral gap, edge expansion, Cheeger inequality, or zig-zag product — so producing an ExpanderFamily is a self-contained sub-project (zig-zag, or a Margulis-type Cayley construction), and everything downstream is already stated against this interface.

Main definitions

• RegGraph.ofRot — a graph on Fin n from a rotation involution
• ExpanderFamily — constant degree, uniform spectral bound, shared label type
• ExpanderFamily.graph, ExpanderFamily.expanderize

Main results

• ExpanderFamily.order_graph, ExpanderFamily.deg_graph
• ExpanderFamily.spectralBound_expanderize — expanderization has a bound
• ExpanderFamily.expanderize_bound_lt_one — and the bound is below one

def Complexity.RegGraph.ofRot (d : ℕ) (hd : 0 < d) (n : ℕ) (rot : Fin n × Fin d → Fin n × Fin d) (hrot : Function.Involutive rot) : RegGraph

The graph on Fin n with labels Fin d given by a rotation involution.

Equations

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

@[simp]

theorem Complexity.RegGraph.order_ofRot (d : ℕ) (hd : 0 < d) (n : ℕ) (rot : Fin n × Fin d → Fin n × Fin d) (hrot : Function.Involutive rot) : (ofRot d hd n rot hrot).order = n

@[simp]

theorem Complexity.RegGraph.deg_ofRot (d : ℕ) (hd : 0 < d) (n : ℕ) (rot : Fin n × Fin d → Fin n × Fin d) (hrot : Function.Involutive rot) : (ofRot d hd n rot hrot).deg = d

structure Complexity.ExpanderFamily : Type

A family of constant-degree expanders, presented as rotation data: for every vertex count n, an involution on Fin n × Fin degree whose graph contracts mean-zero functions by a fixed lam < 1.

• degree : ℕ

  The constant degree, shared by every member.

• degree_pos : 0 < self.degree

  The degree is positive.

• rot (n : ℕ) : Fin n × Fin self.degree → Fin n × Fin self.degree

  The rotation map on n vertices.

• rot_involutive (n : ℕ) : Function.Involutive (self.rot n)

  Each rotation map is an involution.

• lam : ℝ

  The uniform contraction factor.

• lam_nonneg : 0 ≤ self.lam

  The factor is nonnegative.

• lam_lt_one : self.lam < 1

  The factor is below one: this is the spectral gap.

• spectral (n : ℕ) : (RegGraph.ofRot self.degree ⋯ n (self.rot n) ⋯).SpectralBound self.lam

  Every member contracts mean-zero functions by lam.

def Complexity.ExpanderFamily.graph (E : ExpanderFamily) (n : ℕ) : RegGraph

The member of the family on n vertices.

Equations

• E.graph n = Complexity.RegGraph.ofRot E.degree ⋯ n (E.rot n) ⋯

@[simp]

theorem Complexity.ExpanderFamily.V_graph (E : ExpanderFamily) (n : ℕ) : (E.graph n).V = Fin n

@[simp]

theorem Complexity.ExpanderFamily.D_graph (E : ExpanderFamily) (n : ℕ) : (E.graph n).D = Fin E.degree

@[simp]

theorem Complexity.ExpanderFamily.order_graph (E : ExpanderFamily) (n : ℕ) : (E.graph n).order = n

@[simp]

theorem Complexity.ExpanderFamily.deg_graph (E : ExpanderFamily) (n : ℕ) : (E.graph n).deg = E.degree

theorem Complexity.ExpanderFamily.spectral_graph (E : ExpanderFamily) (n : ℕ) : (E.graph n).SpectralBound E.lam

noncomputable def Complexity.ExpanderFamily.vertexEquiv (E : ExpanderFamily) (G : RegGraph) [NumEnc G.V] : (E.graph G.order).V ≃ G.V

The identification of the family member's vertices with G's: the numbering G's vertices carry.

Equations

• E.vertexEquiv G = (Complexity.NumEnc.equivFinCard G.V).symm

noncomputable def Complexity.ExpanderFamily.expanderize (E : ExpanderFamily) (G : RegGraph) [NumEnc G.V] : RegGraph

G with a family expander superposed on its vertices.

Equations

• E.expanderize G = G.union (E.graph G.order) (E.vertexEquiv G)

@[simp]

theorem Complexity.ExpanderFamily.order_expanderize (E : ExpanderFamily) (G : RegGraph) [NumEnc G.V] : (E.expanderize G).order = G.order

@[simp]

theorem Complexity.ExpanderFamily.deg_expanderize (E : ExpanderFamily) (G : RegGraph) [NumEnc G.V] : (E.expanderize G).deg = G.deg + E.degree

theorem Complexity.ExpanderFamily.spectralBound_expanderize (E : ExpanderFamily) (G : RegGraph) [NumEnc G.V] : (E.expanderize G).SpectralBound ((↑G.deg + ↑E.degree * E.lam) / (↑G.deg + ↑E.degree))

Expanderization. Superposing a family expander gives a graph with a spectral bound.

theorem Complexity.ExpanderFamily.expanderize_bound_lt_one (E : ExpanderFamily) (G : RegGraph) : (↑G.deg + ↑E.degree * E.lam) / (↑G.deg + ↑E.degree) < 1

The resulting bound is strictly below one, which is what makes powering gain a factor.