Products of rotation maps

Expanders of constant degree on arbitrarily many vertices are built from small ones by graph products Reingold, Vadhan and Wigderson, Section 1.2 Arora and Barak, Section 21.3 Hoory, Linial and Wigderson, Section 9. Besides powers (Cslib.RotationMap.pow), these are:

• the tensor product G.tensor H on V × V', which takes a step in G and a step in H at the same time: λ(G ⊗ H) ≤ max λ(G) λ(H), with equality when neither factor is empty or without edges;
• the zig-zag product G.zigzag H of a D-regular graph G with a graph H on the labels D of G, on the vertices V × D and with the square of the degree of H: λ(G ⓩ H) ≤ λ(G) + λ(H) + λ(H) ^ 2 and λ(G ⓩ H) ≤ 1 - (1 - λ(G)) (1 - λ(H)) ^ 2;
• the balanced replacement product G.balancedReplacement H, on the same vertices and with twice the degree of H: λ(G Ⓡ H) ^ 3 ≤ 7 / 8 + λ(G ⓩ H) / 8, so that λ(G Ⓡ H) ≤ 1 - (1 - λ(G)) (1 - λ(H)) ^ 2 / 24.

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. The same splitting proves the bound for the tensor product. The walk operator of the balanced replacement product is (B̃ + Ã) / 2, and the zig-zag walk B̃ Ã B̃ is one of the eight terms of its cube Reingold, Vadhan and Wigderson, Theorem 6.7.

Main definitions

• Cslib.RotationMap.tensorRot, Cslib.RotationMap.zigzagRot: the underlying functional rotation programs, shared with their efficiency certificates.
• Cslib.RotationMap.tensor: the tensor product G ⊗ H.
• Cslib.RotationMap.zigzag: the zig-zag product G ⓩ H.
• Cslib.RotationMap.balancedReplacement: the balanced replacement product G Ⓡ H.

Main results

• Cslib.RotationMap.walk_tensor, Cslib.RotationMap.spectralExpansion_tensor_le, Cslib.RotationMap.spectralExpansion_tensor: the walk operator of G ⊗ H is (W_G ⊗ I) (I ⊗ W_H), and its spectral expansion is the larger of those of the factors.
• 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.
• 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
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications

def Cslib.RotationMap.tensorRot {V : Type u_1} {D : Type u_2} {V' : Type u_3} {D' : Type u_4} (rotate : V × D → V × D) (other : V' × D' → V' × D') (p : (V × V') × D × D') : (V × V') × D × D'

Execute a tensor rotation with one call to each component, retaining both return labels.

def Cslib.RotationMap.tensor {V : Type u_1} {D : Type u_2} {V' : Type u_3} {D' : Type u_4} (G : RotationMap V D) (H : RotationMap V' D') : RotationMap (V × V') (D × D')

The tensor product G ⊗ H Reingold, Vadhan and Wigderson, Section 2.3: the multigraph on V × V' with labels D × D' whose edge (i, i') at (v, v') takes the edge i of G at v and the edge i' of H at v' at the same time.

@[simp]

theorem Cslib.RotationMap.rot_tensor {V : Type u_1} {D : Type u_2} {V' : Type u_3} {D' : Type u_4} (G : RotationMap V D) (H : RotationMap V' D') (v : V) (v' : V') (i : D) (i' : D') : (G.tensor H).rot ((v, v'), i, i') = (((G.rot (v, i)).1, (H.rot (v', i')).1), (G.rot (v, i)).2, (H.rot (v', i')).2)

The rotation map of G ⊗ H applies those of G and of H side by side.

@[simp]

theorem Cslib.RotationMap.neighbor_tensor {V : Type u_1} {D : Type u_2} {V' : Type u_3} {D' : Type u_4} (G : RotationMap V D) (H : RotationMap V' D') (p : V × V') (i : D × D') : (G.tensor H).neighbor p i = (G.neighbor p.1 i.1, H.neighbor p.2 i.2)

The neighbors in G ⊗ H are the pairs of a neighbor in G and a neighbor in H.

theorem Cslib.RotationMap.walk_tensor_apply {V : Type u_1} {D : Type u_2} {V' : Type u_3} {D' : Type u_4} (G : RotationMap V D) (H : RotationMap V' D') [Fintype D] [Fintype D'] (f : V × V' → ℝ) (p : V × V') : (G.tensor H).walk f p = Finset.univ.expect fun (i : D) => Finset.univ.expect fun (i' : D') => f (G.neighbor p.1 i, H.neighbor p.2 i')

The walk operator of G ⊗ H averages over a neighbor in G and a neighbor in H.

theorem Cslib.RotationMap.walk_tensor_mul {V : Type u_1} {D : Type u_2} {V' : Type u_3} {D' : Type u_4} (G : RotationMap V D) (H : RotationMap V' D') [Fintype D] [Fintype D'] (f : V → ℝ) (g : V' → ℝ) : ((G.tensor H).walk fun (p : V × V') => f p.1 * g p.2) = fun (p : V × V') => G.walk f p.1 * H.walk g p.2

The walk operator of G ⊗ H is the tensor product of those of G and H: it sends f ⊗ g : (v, v') ↦ f v * g v' to G.walk f ⊗ H.walk g.

theorem Cslib.RotationMap.walk_loops_tensor_apply {V : Type u_1} {V' : Type u_3} {D' : Type u_4} (H : RotationMap V' D') [Fintype D'] (f : V × V' → ℝ) (p : V × V') : ((loops V Unit).tensor H).walk f p = H.walk (fun (w : V') => f (p.1, w)) p.2

The walk operator of (loops V Unit).tensor H is the walk operator I ⊗ W_H of H on every copy {v} × V' of H.

theorem Cslib.RotationMap.walk_tensor_loops_apply {V : Type u_1} {D : Type u_2} {V' : Type u_3} (G : RotationMap V D) [Fintype D] (f : V × V' → ℝ) (p : V × V') : (G.tensor (loops V' Unit)).walk f p = G.walk (fun (w : V) => f (w, p.2)) p.1

The walk operator of G.tensor (loops V' Unit) is the walk operator W_G ⊗ I of G on every copy V × {v'} of G.

theorem Cslib.RotationMap.walk_tensor {V : Type u_1} {D : Type u_2} {V' : Type u_3} {D' : Type u_4} (G : RotationMap V D) (H : RotationMap V' D') [Fintype D] [Fintype D'] : (G.tensor H).walk = (G.tensor (loops V' Unit)).walk ∘ₗ ((loops V Unit).tensor H).walk

The walk operator of G ⊗ H factors as W_G ⊗ W_H = (W_G ⊗ I) (I ⊗ W_H).

theorem Cslib.RotationMap.walk_loops_tensor_comp_fst {V : Type u_1} {V' : Type u_3} {D' : Type u_4} (H : RotationMap V' D') [Fintype D'] [Nonempty D'] (φ : V → ℝ) : (((loops V Unit).tensor H).walk fun (p : V × V') => φ p.1) = fun (p : V × V') => φ p.1

When H has edges, the walk operator on the copies of H fixes the functions that are constant on every copy.

theorem Cslib.RotationMap.expect_walk_loops_tensor_sq_le {V : Type u_1} {V' : Type u_3} {D' : Type u_4} (H : RotationMap V' D') [Fintype D'] [Fintype V] [Fintype V'] {f : V × V' → ℝ} (hf : ∀ (v : V), (Finset.univ.expect fun (v' : V') => f (v, v')) = 0) : (Finset.univ.expect fun (p : V × V') => ((loops V Unit).tensor H).walk f p ^ 2) ≤ H.spectralExpansion ^ 2 * Finset.univ.expect fun (p : V × V') => f p ^ 2

On functions of average zero over every copy {v} × V' of H, the walk operator on the copies of H multiplies the second moment by at most λ(H) ^ 2.

theorem Cslib.RotationMap.spectralExpansion_tensor_le {V : Type u_1} {D : Type u_2} {V' : Type u_3} {D' : Type u_4} (G : RotationMap V D) (H : RotationMap V' D') [Fintype D] [Fintype D'] [Fintype V] [Fintype V'] : (G.tensor H).spectralExpansion ≤ max G.spectralExpansion H.spectralExpansion

The spectral expansion of G ⊗ H is at most the larger of those of G and H Reingold, Vadhan and Wigderson, Proposition 2.4.

theorem Cslib.RotationMap.spectralExpansion_tensor {V : Type u_1} {D : Type u_2} {V' : Type u_3} {D' : Type u_4} (G : RotationMap V D) (H : RotationMap V' D') [Fintype D] [Fintype D'] [Fintype V] [Fintype V'] [Nonempty V] [Nonempty D] [Nonempty V'] [Nonempty D'] : (G.tensor H).spectralExpansion = max G.spectralExpansion H.spectralExpansion

The spectral expansion of G ⊗ H is the larger of those of G and H Reingold, Vadhan and Wigderson, Proposition 2.4, when neither factor is empty or without edges.

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.

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.

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.