The zig-zag tower

A single expander H of constant size generates an infinite family of expanders of constant degree, by alternating squaring with the zig-zag product Reingold, Vadhan and Wigderson, Section 1.2 Hoory, Linial and Wigderson, Section 9.2. Let H be a D-regular multigraph on B, with an equivalence e : B ≃ (Fin 2 → D × D), so that H has |D| ^ 4 vertices. Then

• G₁ = H ^ 2, with its labels Fin 2 → D renamed to D × D;
• Gₙ₊₁ = Gₙ ^ 2 ⓩ H: the square Gₙ ^ 2 has the labels Fin 2 → D × D, which e.symm renames to the vertices B of H, so that it can be zig-zagged with H.

Squaring raises the degree |D| ^ 2 of Gₙ to |D| ^ 4, and the zig-zag product with H brings it back to |D| ^ 2 while multiplying the number of vertices by |B| = |D| ^ 4. So Gₙ is a |D| ^ 2-regular multigraph on |D| ^ (4 n) vertices. If λ(H) ≤ 1 / 5, then λ(Gₙ) ≤ 2 / 5 for every n Reingold, Vadhan and Wigderson, Theorem 1.4: at the start λ(G₁) ≤ λ(H) ^ 2 ≤ 1 / 25, and by the zig-zag theorem Cslib.RotationMap.spectralExpansion_zigzag_le, λ(Gₙ₊₁) ≤ λ(Gₙ) ^ 2 + λ(H) + λ(H) ^ 2 ≤ 4 / 25 + 1 / 5 + 1 / 25 = 2 / 5. More generally, the bound λ(Gₙ) ≤ c is kept whenever c ^ 2 + λ(H) + λ(H) ^ 2 ≤ c.

Here Cslib.RotationMap.zigzagTower H e n is the graph Gₙ₊₁, on the vertices Cslib.RotationMap.ZigzagTowerVertex B n, the (n + 1)-fold product (⋯ (B × B) × ⋯) × B. The tower is explicit given H and e: zigzagTower is a computable definition, which computes the rotation maps of the tower from H.rot, e and e.symm by a recursion without choices; the rotation map of Gₙ₊₁ evaluates that of Gₙ twice and H.rot twice. So H is the only ingredient of the family that may be non-explicit. Evaluating the rotation map of Gₙ takes 2 ^ (n + 1) - 2 evaluations of H.rot, polynomially many in the number of vertices of Gₙ but not in the length of their names: the tower is only mildly explicit Hoory, Linial and Wigderson, Section 9.2, and Reingold, Vadhan and Wigderson interleave tensor products to make it fully explicit Reingold, Vadhan and Wigderson, Section 3.2.

Main definitions

• Cslib.RotationMap.ZigzagTowerVertex: the vertices of the graphs of the tower.
• Cslib.RotationMap.zigzagTower: the zig-zag tower G₁, G₂, … over a base graph H.

Main results

• Cslib.RotationMap.card_zigzagTowerVertex, Cslib.RotationMap.card_zigzagTowerVertex_of_equiv: Gₙ₊₁ has |B| ^ (n + 1) vertices, that is |D| ^ (4 (n + 1)).
• Cslib.RotationMap.lt_card_zigzagTowerVertex: the graphs of the tower grow without bound.
• Cslib.RotationMap.spectralExpansion_zigzagTower_le: if c ^ 2 + λ(H) + λ(H) ^ 2 ≤ c, then every graph of the tower has spectral expansion at most c.
• Cslib.RotationMap.spectralExpansion_zigzagTower_le_two_div_five: if λ(H) ≤ 1 / 5, then every graph of the tower has spectral expansion at most 2 / 5 Reingold, Vadhan and Wigderson, Theorem 1.4.

References

• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications

@[reducible, inline]

abbrev Cslib.RotationMap.ZigzagTowerVertex (B : Type u) : ℕ → Type u

The vertices of the (n + 1)-st graph of the zig-zag tower over a base graph on B: the (n + 1)-fold product (⋯ (B × B) × ⋯) × B, nested to the left, as each zig-zag product pairs a vertex of the previous graph with a vertex of the base graph. They are the iterated products Cslib.RotationMap.ReingoldVertex B B n, whose instances and cardinality apply.

theorem Cslib.RotationMap.card_zigzagTowerVertex (B : Type u) [Fintype B] (n : ℕ) : Fintype.card (ZigzagTowerVertex B n) = Fintype.card B ^ (n + 1)

The (n + 1)-st graph of the tower has |B| ^ (n + 1) vertices.

theorem Cslib.RotationMap.lt_card_zigzagTowerVertex {B : Type u} [Fintype B] (hB : 1 < Fintype.card B) (n : ℕ) : n < Fintype.card (ZigzagTowerVertex B n)

The graphs of the tower grow without bound: if the base graph has at least two vertices, then the (n + 1)-st graph of the tower has more than n vertices.

theorem Cslib.RotationMap.card_zigzagTowerVertex_of_equiv {B : Type u} {D : Type u_1} [Fintype B] [Fintype D] (e : B ≃ (Fin 2 → D × D)) (n : ℕ) : Fintype.card (ZigzagTowerVertex B n) = Fintype.card D ^ (4 * (n + 1))

When the vertices of the base graph name the pairs of pairs of its labels, the (n + 1)-st graph of the tower has |D| ^ (4 (n + 1)) vertices Reingold, Vadhan and Wigderson, Theorem 1.4.

def Cslib.RotationMap.zigzagTower {B : Type u} {D : Type u_1} (H : RotationMap B D) (e : B ≃ (Fin 2 → D × D)) (n : ℕ) : RotationMap (ZigzagTowerVertex B n) (D × D)

The zig-zag tower Reingold, Vadhan and Wigderson, Section 1.2 Hoory, Linial and Wigderson, Section 9.2 over a D-regular base graph H whose vertices name the pairs of pairs of its labels by e. zigzagTower H e n is the graph Gₙ₊₁ of the tower G₁ = H ^ 2, Gₙ₊₁ = Gₙ ^ 2 ⓩ H: the base graph squared, with its labels Fin 2 → D renamed to D × D, and then, at each step, the square of the previous graph, with its labels Fin 2 → D × D renamed by e.symm to the vertices of H, zig-zagged with H.

theorem Cslib.RotationMap.zigzagTower_zero {B : Type u} {D : Type u_1} (H : RotationMap B D) (e : B ≃ (Fin 2 → D × D)) : H.zigzagTower e 0 = (H.pow 2).relabel (finTwoArrowEquiv D)

The first graph of the tower is the base graph squared.

theorem Cslib.RotationMap.zigzagTower_succ {B : Type u} {D : Type u_1} (H : RotationMap B D) (e : B ≃ (Fin 2 → D × D)) (n : ℕ) : H.zigzagTower e (n + 1) = (((H.zigzagTower e n).pow 2).relabel e.symm).zigzag H

Each graph of the tower is the square of the previous one zig-zagged with the base graph.

theorem Cslib.RotationMap.rot_zigzagTower_succ {B : Type u} {D : Type u_1} (H : RotationMap B D) (e : B ≃ (Fin 2 → D × D)) (n : ℕ) (v : ZigzagTowerVertex B n) (k : B) (i j : D) : (H.zigzagTower e (n + 1)).rot ((v, k), i, j) = ((((H.zigzagTower e n).pow 2).relabel e.symm).zigzag H).rot ((v, k), i, j)

The rotation map of each graph of the tower is that of the square of the previous one zig-zagged with the base graph.

theorem Cslib.RotationMap.spectralExpansion_zigzagTower_le {B : Type u} {D : Type u_1} (H : RotationMap B D) (e : B ≃ (Fin 2 → D × D)) [Fintype B] [Fintype D] {c : ℝ} (hc : c ^ 2 + H.spectralExpansion + H.spectralExpansion ^ 2 ≤ c) (n : ℕ) : (H.zigzagTower e n).spectralExpansion ≤ c

The zig-zag tower is a family of expanders: if c ^ 2 + λ(H) + λ(H) ^ 2 ≤ c, then every graph of the tower has spectral expansion at most c.

theorem Cslib.RotationMap.spectralExpansion_zigzagTower_le_two_div_five {B : Type u} {D : Type u_1} (H : RotationMap B D) (e : B ≃ (Fin 2 → D × D)) [Fintype B] [Fintype D] (hH : H.spectralExpansion ≤ 1 / 5) (n : ℕ) : (H.zigzagTower e n).spectralExpansion ≤ 2 / 5

The zig-zag tower is a family of expanders Reingold, Vadhan and Wigderson, Theorem 1.4: if the base graph has spectral expansion at most 1 / 5, then every graph of the tower has spectral expansion at most 2 / 5.