The balanced replacement product of rotation maps

The balanced replacement product G.balancedReplacement H of a D-regular graph G on V with a graph H on the labels D of G is a graph on V × D with twice the degree of H Reingold, Vadhan and Wigderson, Section 6.2 Arora and Barak, Section 21.3. Its walk operator is (B̃ + Ã) / 2, where B̃ = I ⊗ W_H is the walk on the copies {v} × D of H and Ã permutes the vertices by the rotation map of G. Since the zig-zag walk B̃ Ã B̃ is one of the eight terms of its cube, λ(G Ⓡ H) ^ 3 ≤ 7 / 8 + λ(G ⓩ H) / 8, so that λ(G Ⓡ H) ≤ 1 - (1 - λ(G)) (1 - λ(H)) ^ 2 / 24 Reingold, Vadhan and Wigderson, Theorem 6.7.

Main definitions

• Cslib.RotationMap.balancedReplacement: the balanced replacement product G Ⓡ H.

Main results

• Cslib.RotationMap.walk_balancedReplacement: the walk operator of G Ⓡ H is (B̃ + Ã) / 2.
• Cslib.RotationMap.spectralExpansion_balancedReplacement_pow_three_le, Cslib.RotationMap.spectralExpansion_balancedReplacement_le, Cslib.RotationMap.spectralExpansion_balancedReplacement_lt_one: the balanced replacement 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

def Cslib.RotationMap.balancedReplacement {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 balanced replacement product of a D-regular graph G on V with a graph H on the labels D of G Reingold, Vadhan and Wigderson, Definition 6.6 Arora and Barak, Section 21.3. Every vertex v of G is replaced by the copy {v} × D of H. At (v, k), the edge Sum.inl i is the edge i of H at k inside the copy, and the edges Sum.inr i, one for every label i of H, all cross the k-th edge of G at v, to G.rot (v, k). So a step of the random walk takes a step in H or crosses an edge of G with probability 1 / 2 each.

@[simp]

theorem Cslib.RotationMap.rot_balancedReplacement_inl {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) : (G.balancedReplacement H).rot (p, Sum.inl i) = ((p.1, (H.rot (p.2, i)).1), Sum.inl (H.rot (p.2, i)).2)

The edges Sum.inl i of the balanced replacement product are those of H.

@[simp]

theorem Cslib.RotationMap.rot_balancedReplacement_inr {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) : (G.balancedReplacement H).rot (p, Sum.inr i) = (G.rot p, Sum.inr i)

The edges Sum.inr i of the balanced replacement product are those of G.

theorem Cslib.RotationMap.walk_balancedReplacement {V : Type u_1} {D : Type u_2} {E : Type u_3} (G : RotationMap V D) (H : RotationMap D E) [Fintype E] [Nonempty E] : (G.balancedReplacement H).walk = 2⁻¹ • (((loops V Unit).tensor H).walk + LinearMap.funLeft ℝ ℝ G.rot)

When H has edges, the walk operator of the balanced replacement product is (B̃ + Ã) / 2 Reingold, Vadhan and Wigderson, Theorem 6.7, where B̃ = I ⊗ W_H is the walk operator of H on every copy and Ã permutes the vertices V × D by the rotation map of G.

theorem Cslib.RotationMap.spectralExpansion_balancedReplacement_pow_three_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.balancedReplacement H).spectralExpansion ^ 3 ≤ 7 / 8 + (G.zigzag H).spectralExpansion / 8

The cube of the spectral expansion of the balanced replacement product is at most 7 / 8 + λ(G ⓩ H) / 8 Reingold, Vadhan and Wigderson, Theorem 6.7: the zig-zag walk is one of the eight terms of the cube of its walk operator.

theorem Cslib.RotationMap.spectralExpansion_balancedReplacement_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.balancedReplacement H).spectralExpansion ≤ 1 - (1 - G.spectralExpansion) * (1 - H.spectralExpansion) ^ 2 / 24

The spectral expansion of the balanced replacement product is at most 1 - (1 - λ(G)) (1 - λ(H)) ^ 2 / 24: the balanced replacement product of two expanders is an expander.

theorem Cslib.RotationMap.spectralExpansion_balancedReplacement_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.balancedReplacement H).spectralExpansion < 1

The balanced replacement product of two graphs of spectral expansion less than 1 has spectral expansion less than 1 Reingold, Vadhan and Wigderson, Theorem 6.7.