Tensor products of rotation maps

The tensor product G.tensor H of rotation maps on V and V' is the rotation map on V × V' that takes a step in G and a step in H at the same time Reingold, Vadhan and Wigderson, Section 2.3 Arora and Barak, Section 21.3 Hoory, Linial and Wigderson, Section 9. Its walk operator factors as (W_G ⊗ I) (I ⊗ W_H), where I ⊗ W_H is the walk operator of (loops V Unit).tensor H on the copies {v} × V' of H. Splitting a function on V × V' into its averages over the copies of H and a part of average zero on every copy gives λ(G ⊗ H) ≤ max λ(G) λ(H), with equality when neither factor is empty or without edges.

Main definitions

• Cslib.RotationMap.tensorRot: the underlying functional rotation program, shared with its efficiency certificate.
• Cslib.RotationMap.tensor: the tensor product G ⊗ H.

Main results

• Cslib.RotationMap.walk_tensor: the walk operator of G ⊗ H factors as (W_G ⊗ I) (I ⊗ W_H).
• Cslib.RotationMap.spectralExpansion_tensor_le, Cslib.RotationMap.spectralExpansion_tensor: λ(G ⊗ H) ≤ max λ(G) λ(H), with equality when neither factor is empty or without edges.

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.

@[reducible]

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.walk_loops_tensor_add {V : Type u_1} {V' : Type u_3} {D' : Type u_4} (H : RotationMap V' D') [Fintype D'] [Nonempty D'] (φ : V → ℝ) (g : V × V' → ℝ) : (((loops V Unit).tensor H).walk fun (p : V × V') => φ p.1 + g p) = fun (p : V × V') => φ p.1 + ((loops V Unit).tensor H).walk g p

The walk operator on the copies of H acts on the part of average zero over 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.expect_walk_loops_tensor_eq_zero {V : Type u_1} {V' : Type u_3} {D' : Type u_4} (H : RotationMap V' D') [Fintype D'] [Fintype V'] [Nonempty D'] {f : V × V' → ℝ} (hf : ∀ (v : V), (Finset.univ.expect fun (v' : V') => f (v, v')) = 0) (v : V) : (Finset.univ.expect fun (v' : V') => ((loops V Unit).tensor H).walk f (v, v')) = 0

The walk operator on the copies of H keeps average zero over every copy.

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.