The zig-zag product of rotation maps

The zig-zag product G.zigzag H of a D-regular graph G with a graph H on the labels D of G is a graph on V × D with the square of the degree of H Reingold, Vadhan and Wigderson, Section 3 Arora and Barak, Section 21.3 Hoory, Linial and Wigderson, Section 9.3: λ(G ⓩ H) ≤ λ(G) + λ(H) + λ(H) ^ 2 and λ(G ⓩ H) ≤ 1 - (1 - λ(G)) (1 - λ(H)) ^ 2.

The zig-zag theorem is proved as in Reingold, Vadhan and Wigderson, Section 4.1. The walk operator of G ⓩ H is B̃ Ã B̃, where B̃ = I ⊗ W_H is the walk on the copies {v} × D of H, the walk operator of (loops V Unit).tensor H, and Ã permutes the vertices by the rotation map of G. A function on V × D splits into its averages over the copies of H and a part of average zero on every copy; B̃ fixes the first and shrinks the second by λ(H), while on the first Ã acts as the walk on G. This bounds 𝔼 h · W f for every h and every f of expectation zero, and with h = W f it bounds W f: as λ is an operator norm, no eigenvectors are needed.

Main definitions

• Cslib.RotationMap.zigzagRot: the underlying functional rotation program, shared with its efficiency certificate.
• Cslib.RotationMap.zigzag: the zig-zag product G ⓩ H.

Main results

• Cslib.RotationMap.walk_zigzag: the walk operator of G ⓩ H is B̃ Ã B̃.
• Cslib.RotationMap.spectralExpansion_zigzag_le: the zig-zag theorem, λ(G ⓩ H) ≤ λ(G) + λ(H) + λ(H) ^ 2.
• Cslib.RotationMap.spectralExpansion_zigzag_le_one_sub, Cslib.RotationMap.spectralExpansion_zigzag_lt_one: the zig-zag product of two expanders is an expander.

References

• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications

def Cslib.RotationMap.zigzagRot {V : Type u_1} {D : Type u_2} {E : Type u_3} (rotate : V × D → V × D) (cloud : D × E → D × E) (p : (V × D) × E × E) : (V × D) × E × E

Execute a zig-zag rotation, retaining the return labels of the zig and zag.

@[reducible]

def Cslib.RotationMap.zigzag {V : Type u_1} {D : Type u_2} {E : Type u_3} (G : RotationMap V D) (H : RotationMap D E) : RotationMap (V × D) (E × E)

The zig-zag product G ⓩ H Reingold, Vadhan and Wigderson, Definition 3.1 Hoory, Linial and Wigderson, Section 9.3 of a D-regular graph G on V with a graph H on the labels D of G. Its vertices are the pairs (v, k), the k-th edge at v, grouped into the cloud {v} × D of v, and its labels are pairs of labels of H. The edge (i, j) at (v, k) takes the edge i of H from k to k' inside the cloud ("zig"), crosses the k'-th edge of G from v to (w, ℓ'), where it is the ℓ'-th edge at w, and takes the edge j of H from ℓ' to ℓ inside the cloud of w ("zag"), ending at (w, ℓ).

@[simp]

theorem Cslib.RotationMap.rot_zigzag {V : Type u_1} {D : Type u_2} {E : Type u_3} (G : RotationMap V D) (H : RotationMap D E) (v : V) (k : D) (i j : E) : (G.zigzag H).rot ((v, k), i, j) = (((G.rot (v, (H.rot (k, i)).1)).1, (H.rot ((G.rot (v, (H.rot (k, i)).1)).2, j)).1), (H.rot ((G.rot (v, (H.rot (k, i)).1)).2, j)).2, (H.rot (k, i)).2)

The rotation map of G ⓩ H Reingold, Vadhan and Wigderson, Definition 3.1: with (k', i') = H.rot (k, i), (w, ℓ') = G.rot (v, k') and (ℓ, j') = H.rot (ℓ', j), the edge (i, j) at (v, k) is the edge (j', i') at (w, ℓ).

theorem Cslib.RotationMap.neighbor_zigzag {V : Type u_1} {D : Type u_2} {E : Type u_3} (G : RotationMap V D) (H : RotationMap D E) (p : V × D) (i : E × E) : (G.zigzag H).neighbor p i = ((G.rot (p.1, H.neighbor p.2 i.1)).1, H.neighbor (G.rot (p.1, H.neighbor p.2 i.1)).2 i.2)

The neighbors in G ⓩ H: a step in H, a step in G, and a step in H.

theorem Cslib.RotationMap.walk_zigzag {V : Type u_1} {D : Type u_2} {E : Type u_3} (G : RotationMap V D) (H : RotationMap D E) [Fintype E] : (G.zigzag H).walk = ((loops V Unit).tensor H).walk ∘ₗ LinearMap.funLeft ℝ ℝ G.rot ∘ₗ ((loops V Unit).tensor H).walk

The walk operator of G ⓩ H is B̃ Ã B̃ Reingold, Vadhan and Wigderson, Section 4.1, where B̃ = I ⊗ W_H is the walk operator of H on every cloud and Ã is the permutation of the vertices V × D by the rotation map of G.

theorem Cslib.RotationMap.spectralExpansion_zigzag_le {V : Type u_1} {D : Type u_2} {E : Type u_3} (G : RotationMap V D) (H : RotationMap D E) [Fintype E] [Fintype V] [Fintype D] : (G.zigzag H).spectralExpansion ≤ G.spectralExpansion + H.spectralExpansion + H.spectralExpansion ^ 2

The zig-zag theorem Reingold, Vadhan and Wigderson, Theorem 3.2 Hoory, Linial and Wigderson, Section 9.3: the spectral expansion of G ⓩ H is at most λ(G) + λ(H) + λ(H) ^ 2.

theorem Cslib.RotationMap.spectralExpansion_zigzag_le_one_sub {V : Type u_1} {D : Type u_2} {E : Type u_3} (G : RotationMap V D) (H : RotationMap D E) [Fintype E] [Fintype V] [Fintype D] : (G.zigzag H).spectralExpansion ≤ 1 - (1 - G.spectralExpansion) * (1 - H.spectralExpansion) ^ 2

The spectral expansion of G ⓩ H is at most 1 - (1 - λ(G)) (1 - λ(H)) ^ 2: the zig-zag product of two expanders is an expander. This form of the bound is useful when λ(G) and λ(H) are close to 1.

theorem Cslib.RotationMap.spectralExpansion_zigzag_lt_one {V : Type u_1} {D : Type u_2} {E : Type u_3} (G : RotationMap V D) (H : RotationMap D E) [Fintype E] [Fintype V] [Fintype D] (hG : G.spectralExpansion < 1) (hH : H.spectralExpansion < 1) : (G.zigzag H).spectralExpansion < 1

The zig-zag product of two graphs of spectral expansion less than 1 has spectral expansion less than 1 Reingold, Vadhan and Wigderson, Theorem 3.2.