Regular graphs, their walk operator, and the spectral gap

The graph-theoretic substrate of Dinur's proof: regular multigraphs given by a rotation map, the associated random-walk averaging operator, and a square-norm formulation of the spectral gap.

A RegGraph carries a finite vertex type V, a finite nonempty label type D, and an involution rot : V × D → V × D on darts (a vertex together with one of its outgoing edge labels). The involution pairs each dart with its reverse, which is what makes the graph undirected and |D|-regular, with parallel edges and self-loops allowed — all three are needed, since powering and expanderization produce them. The neighbour function is nbr v i = (rot (v,i)).1.

Why V and D are types, not numbers

Dinur's constructions build new graphs whose vertices and labels are structured: powering takes the label type to walk tuples Fin t → D, and degree reduction takes the vertex type to the dart type V × D. Carrying V and D as types lets those constructions be written directly, with no encoding bijections; the translation to Fin-indexed data is deferred to the one place that needs it, the encoded reduction at the very end.

The spectral gap, without square roots

Rather than second eigenvalues, SpectralBound G lam says directly that the walk operator contracts mean-zero functions by lam in the Euclidean norm, stated on squared norms:

∑ v, (step f v) ^ 2 ≤ lam ^ 2 * ∑ v, (f v) ^ 2 whenever ∑ v, f v = 0.

This avoids Real.sqrt and eigenvalue machinery entirely, and it is exactly the form the walk analysis needs: step preserves sums (so it preserves mean-zero-ness), hence the bound self-composes and t steps contract by lam ^ t.

Main definitions

• RegGraph, RegGraph.deg, RegGraph.order, RegGraph.nbr, RegGraph.step, RegGraph.stepIter
• RegGraph.SpectralBound

Main results

• RegGraph.sum_nbr — summing over darts is summing over vertices, deg times
• RegGraph.sum_step — the walk operator preserves sums
• RegGraph.step_symm — it is self-adjoint
• RegGraph.sum_sq_step_le — it is a contraction, with no spectral hypothesis
• RegGraph.sum_sq_stepIter_le — t steps contract mean-zero functions by lam ^ (2 * t) in squared norm

structure Complexity.RegGraph : Type 1

A regular multigraph, presented by a rotation map: an involution on darts (vertex, edge label) sending each dart to its reverse. Every vertex has exactly one dart per label, so the graph is |D|-regular; parallel edges and self-loops are allowed.

• V : Type

  The vertex type.

• D : Type

  The edge-label type; each vertex has one outgoing dart per label.

• decEqV : DecidableEq self.V

  Vertices have decidable equality, so assignments form a Fintype.

• decEqD : DecidableEq self.D

  Labels have decidable equality, so label tuples form a Fintype.

• fintypeV : Fintype self.V

  The vertex type is finite.

• fintypeD : Fintype self.D

  The label type is finite.

• nonemptyD : Nonempty self.D

  The label type is nonempty, i.e. the degree is positive.

• rot : self.V × self.D → self.V × self.D

  The rotation map, sending a dart to its reverse.

• rot_involutive : Function.Involutive self.rot

  Reversing a dart twice is the identity.

def Complexity.RegGraph.deg (G : RegGraph) : ℕ

The degree: the number of darts at each vertex.

Equations

• G.deg = Fintype.card G.D

def Complexity.RegGraph.order (G : RegGraph) : ℕ

The number of vertices.

Equations

• G.order = Fintype.card G.V

theorem Complexity.RegGraph.deg_pos (G : RegGraph) : 0 < G.deg

@[simp]

theorem Complexity.RegGraph.card_eq_order (G : RegGraph) : Fintype.card G.V = G.order

@[simp]

theorem Complexity.RegGraph.card_eq_deg (G : RegGraph) : Fintype.card G.D = G.deg

theorem Complexity.RegGraph.deg_ne_zero (G : RegGraph) : ↑G.deg ≠ 0

def Complexity.RegGraph.nbr (G : RegGraph) (v : G.V) (i : G.D) : G.V

The i-th neighbour of v.

Equations

• G.nbr v i = (G.rot (v, i)).1

theorem Complexity.RegGraph.rot_bijective (G : RegGraph) : Function.Bijective G.rot

The rotation map is a bijection of darts.

theorem Complexity.RegGraph.sum_nbr_nsmul (G : RegGraph) {M : Type u_1} [AddCommMonoid M] (f : G.V → M) : ∑ v : G.V, ∑ i : G.D, f (G.nbr v i) = G.deg • ∑ v : G.V, f v

Summing a function of the neighbour over all darts is summing it over all vertices, each counted deg times. This is the rotation-map form of regularity, and it is the source of every counting identity below. Stated for an arbitrary AddCommMonoid, since the walk analysis needs it both for real averages and for counting in ℕ.

theorem Complexity.RegGraph.sum_nbr (G : RegGraph) (f : G.V → ℝ) : ∑ v : G.V, ∑ i : G.D, f (G.nbr v i) = ↑G.deg * ∑ v : G.V, f v

noncomputable def Complexity.RegGraph.step (G : RegGraph) (f : G.V → ℝ) (v : G.V) : ℝ

One step of the random walk, as an averaging operator on real-valued functions on the vertices.

Equations

• G.step f v = (∑ i : G.D, f (G.nbr v i)) / ↑G.deg

theorem Complexity.RegGraph.sum_step (G : RegGraph) (f : G.V → ℝ) : ∑ v : G.V, G.step f v = ∑ v : G.V, f v

The walk operator preserves sums: it is doubly stochastic.

theorem Complexity.RegGraph.step_symm (G : RegGraph) (f g : G.V → ℝ) : ∑ v : G.V, G.step f v * g v = ∑ v : G.V, f v * G.step g v

The walk operator is self-adjoint for the standard inner product.

noncomputable def Complexity.RegGraph.stepIter (G : RegGraph) (t : ℕ) (f : G.V → ℝ) : G.V → ℝ

The t-step walk operator.

Equations

• G.stepIter t f = G.step^[t] f

@[simp]

theorem Complexity.RegGraph.stepIter_zero (G : RegGraph) (f : G.V → ℝ) : G.stepIter 0 f = f

theorem Complexity.RegGraph.stepIter_succ (G : RegGraph) (t : ℕ) (f : G.V → ℝ) : G.stepIter (t + 1) f = G.step (G.stepIter t f)

theorem Complexity.RegGraph.stepIter_succ' (G : RegGraph) (t : ℕ) (f : G.V → ℝ) : G.stepIter (t + 1) f = G.stepIter t (G.step f)

theorem Complexity.RegGraph.sum_stepIter (G : RegGraph) (t : ℕ) (f : G.V → ℝ) : ∑ v : G.V, G.stepIter t f v = ∑ v : G.V, f v

theorem Complexity.RegGraph.sum_sq_step_le (G : RegGraph) (f : G.V → ℝ) : ∑ v : G.V, G.step f v ^ 2 ≤ ∑ v : G.V, f v ^ 2

The walk operator is a contraction. Averaging can only shrink the Euclidean norm — this is Cauchy–Schwarz on each vertex's average, summed with sum_nbr. It holds for every regular graph, with no spectral assumption, and is what lets a graph be combined with an expander: the graph's own part of the combined walk contributes at most its full weight.

def Complexity.RegGraph.SpectralBound (G : RegGraph) (lam : ℝ) : Prop

G has spectral gap at least 1 - lam: the walk operator contracts every mean-zero function by a factor lam in the Euclidean norm, stated on squared norms so that no square roots are needed.

Equations

• G.SpectralBound lam = ∀ (f : G.V → ℝ), ∑ v : G.V, f v = 0 → ∑ v : G.V, G.step f v ^ 2 ≤ lam ^ 2 * ∑ v : G.V, f v ^ 2

theorem Complexity.RegGraph.SpectralBound.mono {G : RegGraph} {lam lam' : ℝ} (h : G.SpectralBound lam) (h0 : 0 ≤ lam) (hle : lam ≤ lam') : G.SpectralBound lam'

A weaker contraction factor is still a contraction factor.

theorem Complexity.RegGraph.spectralBound_of_isEmpty {G : RegGraph} (h : IsEmpty G.V) (lam : ℝ) : G.SpectralBound lam

Every graph contracts the empty family of mean-zero functions: a graph with no vertices has any contraction factor.

theorem Complexity.RegGraph.sum_sq_stepIter_le (G : RegGraph) {lam : ℝ} (h : G.SpectralBound lam) (t : ℕ) (f : G.V → ℝ) (hf : ∑ v : G.V, f v = 0) : ∑ v : G.V, G.stepIter t f v ^ 2 ≤ lam ^ (2 * t) * ∑ v : G.V, f v ^ 2

The contraction self-composes: t steps contract a mean-zero function by lam ^ t, i.e. lam ^ (2 * t) in squared norm.