Powers of rotation maps

The t-th power G ^ t of a D-regular multigraph G has an edge for every walk of length t in G Reingold, Vadhan and Wigderson, Section 2.3 Arora and Barak, Section 21.3. Its labels are the t-tuples of labels of G, and its rotation map follows the walk and reverses it, so that the labels at the far end describe the walk back. A step of the random walk on G ^ t is t steps of the random walk on G: the walk operator of G ^ t is the t-th power of that of G, and λ(G ^ t) = λ(G) ^ t for t ≠ 0.

The bound λ(G ^ t) ≤ λ(G) ^ t holds as for any operator norm. For the reverse inequality, which spectral theory would give at once, the second moments a s = 𝔼 v, (G.walk ^ s) f v ^ 2 along the walk from a function f are log-convex, as the walk operator is self-adjoint, so that a 0 * a 1 ^ t ≤ a 0 ^ t * a t.

Main definitions

• Cslib.RotationMap.powRot: the rotation map of the walks of length t.
• Cslib.RotationMap.pow: the t-th power G ^ t, with labels Fin t → D.

Main results

• Cslib.RotationMap.powRot_involutive: reversing a walk twice gives it back.
• Cslib.RotationMap.rot_pow_succ, Cslib.RotationMap.neighbor_pow_succ, Cslib.RotationMap.neighbor_pow_succ': a walk of length t + 1 is a step followed by a walk of length t, and a walk of length t followed by a step.
• Cslib.RotationMap.walk_pow: the walk operator of G ^ t is the t-th power of that of G.
• Cslib.RotationMap.spectralExpansion_pow_le, Cslib.RotationMap.spectralExpansion_pow: λ(G ^ t) ≤ λ(G) ^ t, with equality for t ≠ 0.

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.powRot {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (t : ℕ) : V × (Fin t → D) → V × (Fin t → D)

The rotation map of the walks of length t in G Reingold, Vadhan and Wigderson, Section 2.3: G.powRot t (v, k) = (w, ℓ) when the walk from v along the labels k 0, …, k (t - 1) ends at w, and ℓ lists the labels of its edges at their far ends, from the last edge back to the first, so that ℓ labels the reverse walk from w to v.

@[simp]

theorem Cslib.RotationMap.powRot_zero {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (p : V × (Fin 0 → D)) : G.powRot 0 p = p

A walk of length 0 is the identity.

theorem Cslib.RotationMap.powRot_succ {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (t : ℕ) (p : V × (Fin (t + 1) → D)) : G.powRot (t + 1) p = ((G.powRot t ((G.rot (p.1, p.2 0)).1, Fin.tail p.2)).1, Fin.snoc (G.powRot t ((G.rot (p.1, p.2 0)).1, Fin.tail p.2)).2 (G.rot (p.1, p.2 0)).2)

A walk of length t + 1 is a first step followed by a walk of length t.

theorem Cslib.RotationMap.powRot_involutive {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (t : ℕ) : Function.Involutive (G.powRot t)

Reversing a walk twice returns the original walk.

def Cslib.RotationMap.pow {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (t : ℕ) : RotationMap V (Fin t → D)

The t-th power G ^ t Reingold, Vadhan and Wigderson, Section 2.3: the multigraph on the same vertices with an edge for every walk of length t in G, labelled by the labels of its steps.

@[simp]

theorem Cslib.RotationMap.rot_pow_zero {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (p : V × (Fin 0 → D)) : (G.pow 0).rot p = p

In G ^ 0, the rotation map is the identity.

theorem Cslib.RotationMap.rot_pow_succ {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (t : ℕ) (p : V × (Fin (t + 1) → D)) : (G.pow (t + 1)).rot p = (((G.pow t).rot ((G.rot (p.1, p.2 0)).1, Fin.tail p.2)).1, Fin.snoc ((G.pow t).rot ((G.rot (p.1, p.2 0)).1, Fin.tail p.2)).2 (G.rot (p.1, p.2 0)).2)

In G ^ (t + 1), the rotation map takes the first edge and then reverses the remaining walk, appending the return label of the first edge at the end.

@[simp]

theorem Cslib.RotationMap.neighbor_pow_zero {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (v : V) (k : Fin 0 → D) : (G.pow 0).neighbor v k = v

In G ^ 0, every edge is a self-loop.

theorem Cslib.RotationMap.neighbor_pow_succ {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (t : ℕ) (v : V) (k : Fin (t + 1) → D) : (G.pow (t + 1)).neighbor v k = (G.pow t).neighbor (G.neighbor v (k 0)) (Fin.tail k)

In G ^ (t + 1), the walk along k takes the edge k 0 and then the walk along the remaining labels.

theorem Cslib.RotationMap.neighbor_pow_succ' {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (t : ℕ) (v : V) (k : Fin (t + 1) → D) : (G.pow (t + 1)).neighbor v k = G.neighbor ((G.pow t).neighbor v (Fin.init k)) (k (Fin.last t))

In G ^ (t + 1), the walk along k takes the walk along all labels but the last, then the edge labelled by the last.

theorem Cslib.RotationMap.walk_pow {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] (t : ℕ) : (G.pow t).walk = G.walk ^ t

The walk operator of G ^ t is the t-th power of that of G.

theorem Cslib.RotationMap.spectralExpansion_pow_le {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] (t : ℕ) : (G.pow t).spectralExpansion ≤ G.spectralExpansion ^ t

The spectral expansion of G ^ t is at most λ(G) ^ t Reingold, Vadhan and Wigderson, Proposition 2.3.

theorem Cslib.RotationMap.spectralExpansion_pow {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] {t : ℕ} (ht : t ≠ 0) : (G.pow t).spectralExpansion = G.spectralExpansion ^ t

The spectral expansion of G ^ t is λ(G) ^ t, for t ≠ 0 Reingold, Vadhan and Wigderson, Proposition 2.3.