Superposing two graphs, and expanderization

Dinur's preprocessing turns an arbitrary regular constraint graph into one that is also an expander, by laying an expander over the same vertex set and taking the union of the two edge sets. This module builds that union and bounds its spectral gap.

The union of a graph G with a graph H — identified with G's vertices along a bijection e — has label type G.D ⊕ H.D and degree G.deg + H.deg. Its walk operator is the weighted average of the two:

step_U f = (G.deg • step_G f + H.deg • step_H (f ∘ e)) / (G.deg + H.deg)

so if H contracts mean-zero functions by lam, the union contracts them by (G.deg + H.deg * lam) / (G.deg + H.deg) — strictly below one whenever lam is — using nothing about G beyond sum_sq_step_le, that its own walk operator is a contraction.

Staying square-root-free

The triangle inequality looks unavailable in the squared-norm formulation, but it is not needed. Expanding ‖aX + bY‖² leaves a cross term ⟨X, Y⟩, and Cauchy–Schwarz bounds its square by ‖X‖² ‖Y‖² ≤ A · lam² A = (lam A)² — whose square root, lam A, is rational in the data. So the cross term is bounded with one application of le_of_sq_le_sq and no Real.sqrt ever appears.

Main definitions

• RegGraph.unionRot — the rotation map of the union
• RegGraph.union — the union graph

Main results

• RegGraph.deg_union, RegGraph.step_union
• RegGraph.sum_sq_step_union_le — the combined contraction bound
• RegGraph.spectralBound_union — expanderization: laying an expander over any regular graph gives a spectral bound strictly below one

def Complexity.RegGraph.unionRot (G H : RegGraph) (e : H.V ≃ G.V) : G.V × (G.D ⊕ H.D) → G.V × (G.D ⊕ H.D)

The rotation map of the union: reverse within G, or within H after transporting along e.

Equations

• G.unionRot H e (v, Sum.inl i) = ((G.rot (v, i)).1, Sum.inl (G.rot (v, i)).2)
• G.unionRot H e (v, Sum.inr j) = (e (H.rot (e.symm v, j)).1, Sum.inr (H.rot (e.symm v, j)).2)

theorem Complexity.RegGraph.unionRot_involutive (G H : RegGraph) (e : H.V ≃ G.V) : Function.Involutive (G.unionRot H e)

def Complexity.RegGraph.union (G H : RegGraph) (e : H.V ≃ G.V) : RegGraph

The union of G with H, whose vertices are identified with G's along e: the edge sets are superposed.

Equations

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

@[simp]

theorem Complexity.RegGraph.V_union (G H : RegGraph) (e : H.V ≃ G.V) : (G.union H e).V = G.V

@[simp]

theorem Complexity.RegGraph.order_union (G H : RegGraph) (e : H.V ≃ G.V) : (G.union H e).order = G.order

@[simp]

theorem Complexity.RegGraph.deg_union (G H : RegGraph) (e : H.V ≃ G.V) : (G.union H e).deg = G.deg + H.deg

theorem Complexity.RegGraph.nbr_union_inl (G H : RegGraph) (e : H.V ≃ G.V) (v : G.V) (i : G.D) : (G.union H e).nbr v (Sum.inl i) = G.nbr v i

theorem Complexity.RegGraph.nbr_union_inr (G H : RegGraph) (e : H.V ≃ G.V) (v : G.V) (j : H.D) : (G.union H e).nbr v (Sum.inr j) = e (H.nbr (e.symm v) j)

theorem Complexity.RegGraph.step_union (G H : RegGraph) (e : H.V ≃ G.V) (f : G.V → ℝ) (v : G.V) : (G.union H e).step f v = (↑G.deg * G.step f v + ↑H.deg * H.step (fun (u : H.V) => f (e u)) (e.symm v)) / (↑G.deg + ↑H.deg)

The union's walk operator is the degree-weighted average of the two walk operators, the second read through the identification e.

The combined contraction bound

theorem Complexity.RegGraph.sum_sq_step_union_le (G H : RegGraph) (e : H.V ≃ G.V) {lam : ℝ} (hlam : 0 ≤ lam) (hH : H.SpectralBound lam) (f : G.V → ℝ) (hf : ∑ v : G.V, f v = 0) : ∑ v : G.V, (G.union H e).step f v ^ 2 ≤ ((↑G.deg + ↑H.deg * lam) / (↑G.deg + ↑H.deg)) ^ 2 * ∑ v : G.V, f v ^ 2

Expanderization, quantitatively. If H contracts mean-zero functions by lam, then the union contracts them by the degree-weighted average of 1 and lam.

theorem Complexity.RegGraph.spectralBound_union (G H : RegGraph) (e : H.V ≃ G.V) {lam : ℝ} (hlam : 0 ≤ lam) (hH : H.SpectralBound lam) : (G.union H e).SpectralBound ((↑G.deg + ↑H.deg * lam) / (↑G.deg + ↑H.deg))

Expanderization.