Rotation maps and the spectral expansion of regular graphs

A D-regular undirected multigraph on V, with parallel edges and self-loops allowed, is presented by its rotation map Reingold, Vadhan and Wigderson, Section 2.1 Arora and Barak, Section 21.3 rot : V × D → V × D: rot (v, i) = (w, j) when the i-th edge at v leads to w and is the j-th edge at w. Following an edge back returns to where it started, so rot is an involution; conversely every involution of V × D is the rotation map of a D-regular multigraph. Vertices and labels are types rather than numbers because graph products build graphs whose vertices and labels are pairs or tuples of those of their factors.

The random walk on G moves from v along a uniformly random edge. Its action on real functions is the walk operator G.walk, which averages a function over the neighbors of each vertex; it fixes constants, preserves expectations, is self-adjoint for the uniform inner product 𝔼 v, f v * g v and does not increase 𝔼 v, f v ^ 2.

The spectral expansion λ(G) Arora and Barak, Section 21.1 is the operator norm of the walk operator on the functions orthogonal to the constants: the smallest c ≥ 0 with 𝔼 v, G.walk f v ^ 2 ≤ c ^ 2 * 𝔼 v, f v ^ 2 for all f of expectation zero (spectralExpansion_le_iff). It is the largest absolute value of an eigenvalue of the walk operator on such functions, but no spectral theory is needed here: everything below is proved from this characterization. λ(G) ≤ 1 always, and G is a good expander when λ(G) is small.

Main definitions

• Cslib.RotationMap: a D-regular multigraph on V, given by its rotation map.
• Cslib.RotationMap.neighbor: the i-th neighbor of a vertex.
• Cslib.RotationMap.ofInvolutive: the 1-regular multigraph of an involution.
• Cslib.RotationMap.interedges: the edges from one set of vertices to another, as darts.
• Cslib.RotationMap.walk: the walk operator.
• Cslib.RotationMap.spectralExpansion: the spectral expansion λ(G).

Main results

• Cslib.RotationMap.expect_expect_neighbor_comm: every edge is seen once from each of its ends.
• Cslib.RotationMap.expect_walk, Cslib.RotationMap.expect_mul_walk_comm, Cslib.RotationMap.expect_walk_sq_le: the walk operator preserves expectations, is self-adjoint and does not increase the second moment.
• Cslib.RotationMap.spectralExpansion_le_iff: the characterization of λ(G).
• Cslib.RotationMap.expect_walk_pow_sq_le_spectralExpansion_pow_mul: walks of length t multiply the second moment of a function of expectation zero by at most λ(G) ^ (2 t).
• Cslib.RotationMap.spectralExpansion_le_one: λ(G) ≤ 1.
• Cslib.RotationMap.spectralExpansion_eq_of_walk_eq: two regular multigraphs with the same walk operator have the same spectral expansion.

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

structure Cslib.RotationMap (V : Type u_1) (D : Type u_2) : Type (max u_1 u_2)

A D-regular undirected multigraph on V, parallel edges and self-loops allowed, presented by its rotation map Reingold, Vadhan and Wigderson, Section 2.1 Arora and Barak, Section 21.3: rot (v, i) = (w, j) when the i-th edge at v leads to w and is the j-th edge at w.

• rot : V × D → V × D

  The rotation map, sending the i-th edge at v to the same edge seen from its other end.

• rot_involutive : Function.Involutive self.rot

  Seeing an edge from its other end twice returns to the original end.

theorem Cslib.RotationMap.ext {V : Type u_1} {D : Type u_2} {x y : RotationMap V D} (rot : x.rot = y.rot) : x = y

theorem Cslib.RotationMap.ext_iff {V : Type u_1} {D : Type u_2} {x y : RotationMap V D} : x = y ↔ x.rot = y.rot

@[simp]

theorem Cslib.RotationMap.rot_rot {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (p : V × D) : G.rot (G.rot p) = p

Seeing an edge from its other end twice returns to the original end.

def Cslib.RotationMap.neighbor {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (v : V) (i : D) : V

The i-th neighbor of v: the other end of the i-th edge at v.

theorem Cslib.RotationMap.neighbor_def {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (v : V) (i : D) : G.neighbor v i = (G.rot (v, i)).1

The i-th neighbor of v is the first component of the rotation map at (v, i).

def Cslib.RotationMap.ofInvolutive {V : Type u_1} (f : V → V) (hf : Function.Involutive f) : RotationMap V Unit

The 1-regular multigraph of an involution f: the single edge at v leads to f v. A fixed point of f carries a self-loop.

@[simp]

theorem Cslib.RotationMap.rot_ofInvolutive {V : Type u_1} (f : V → V) (hf : Function.Involutive f) (p : V × Unit) : (ofInvolutive f hf).rot p = (f p.1, p.2)

The rotation map of the multigraph of an involution f applies f to the vertex.

@[simp]

theorem Cslib.RotationMap.neighbor_ofInvolutive {V : Type u_1} (f : V → V) (hf : Function.Involutive f) (v : V) (i : Unit) : (ofInvolutive f hf).neighbor v i = f v

The neighbor of v in the multigraph of an involution f is f v.

@[simp]

theorem Cslib.RotationMap.neighbor_neighbor_rot {V : Type u_1} {D : Type u_2} (G : RotationMap V D) (v : V) (i : D) : G.neighbor (G.neighbor v i) (G.rot (v, i)).2 = v

v is the neighbor of its i-th neighbor along the same edge.

def Cslib.RotationMap.interedges {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [DecidableEq V] [Fintype D] (S T : Finset V) : Finset (V × D)

The edges from S to T, as the darts (v, i) with v ∈ S whose i-th edge leads into T. An edge between two vertices of S ∩ T is counted once from each end, as in the edge counts |E(S, T)| of Hoory, Linial and Wigderson, Section 2.1.

@[simp]

theorem Cslib.RotationMap.mem_interedges {V : Type u_1} {D : Type u_2} {G : RotationMap V D} [DecidableEq V] [Fintype D] {S T : Finset V} {p : V × D} : p ∈ G.interedges S T ↔ p.1 ∈ S ∧ G.neighbor p.1 p.2 ∈ T

A dart (v, i) goes from S to T when v ∈ S and its i-th neighbor is in T.

@[simp]

theorem Cslib.RotationMap.interedges_empty_left {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [DecidableEq V] [Fintype D] (T : Finset V) : G.interedges ∅ T = ∅

No edges leave the empty set.

@[simp]

theorem Cslib.RotationMap.interedges_empty_right {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [DecidableEq V] [Fintype D] (S : Finset V) : G.interedges S ∅ = ∅

No edges enter the empty set.

theorem Cslib.RotationMap.card_interedges_comm {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [DecidableEq V] [Fintype D] (S T : Finset V) : (G.interedges S T).card = (G.interedges T S).card

Reversing the darts matches the edges from S to T with those from T to S.

theorem Cslib.RotationMap.card_interedges_add_card_interedges_compl {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [DecidableEq V] [Fintype D] [Fintype V] (S T : Finset V) : (G.interedges S T).card + (G.interedges S Tᶜ).card = S.card * Fintype.card D

Every edge at a vertex of S leads into T or into its complement.

theorem Cslib.RotationMap.expect_expect_neighbor_comm {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (F : V → V → M) : (Finset.univ.expect fun (v : V) => Finset.univ.expect fun (i : D) => F v (G.neighbor v i)) = Finset.univ.expect fun (v : V) => Finset.univ.expect fun (i : D) => F (G.neighbor v i) v

Every edge is seen once from each of its ends: averaging F v (G.neighbor v i) over the darts (v, i) gives the same as averaging F (G.neighbor v i) v.

theorem Cslib.RotationMap.expect_comp_rot {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (u : V × D → M) : (Finset.univ.expect fun (q : V × D) => u (G.rot q)) = Finset.univ.expect fun (q : V × D) => u q

The rotation map permutes the darts, so it preserves averages over them.

theorem Cslib.RotationMap.expect_expect_neighbor {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] [Nonempty D] (f : V → M) : (Finset.univ.expect fun (v : V) => Finset.univ.expect fun (i : D) => f (G.neighbor v i)) = Finset.univ.expect fun (v : V) => f v

Averaging a function of the neighbor over all darts averages it over the vertices.

noncomputable def Cslib.RotationMap.walk {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] : (V → ℝ) →ₗ[ℝ] V → ℝ

The walk operator of G: G.walk f v is the average of f over the neighbors of v, the expected value of f after one step of the random walk from v.

theorem Cslib.RotationMap.walk_apply {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] (f : V → ℝ) (v : V) : G.walk f v = Finset.univ.expect fun (i : D) => f (G.neighbor v i)

G.walk f v is the average of f over the neighbors of v.

@[simp]

theorem Cslib.RotationMap.walk_const {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Nonempty D] (c : ℝ) : (G.walk fun (x : V) => c) = fun (x : V) => c

The walk operator fixes constants.

@[simp]

theorem Cslib.RotationMap.walk_pow_const {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Nonempty D] (t : ℕ) (c : ℝ) : ((G.walk ^ t) fun (x : V) => c) = fun (x : V) => c

Walks of every length fix constants.

@[simp]

theorem Cslib.RotationMap.expect_walk {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] [Nonempty D] (f : V → ℝ) : (Finset.univ.expect fun (v : V) => G.walk f v) = Finset.univ.expect fun (v : V) => f v

The walk operator preserves expectations.

@[simp]

theorem Cslib.RotationMap.expect_walk_pow {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] [Nonempty D] (t : ℕ) (f : V → ℝ) : (Finset.univ.expect fun (v : V) => (G.walk ^ t) f v) = Finset.univ.expect fun (v : V) => f v

Walks of every length preserve expectations.

theorem Cslib.RotationMap.expect_walk_eq_zero {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] {f : V → ℝ} (hf : (Finset.univ.expect fun (v : V) => f v) = 0) : (Finset.univ.expect fun (v : V) => G.walk f v) = 0

The walk operator preserves expectation zero.

theorem Cslib.RotationMap.expect_walk_pow_eq_zero {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] {f : V → ℝ} (hf : (Finset.univ.expect fun (v : V) => f v) = 0) (t : ℕ) : (Finset.univ.expect fun (v : V) => (G.walk ^ t) f v) = 0

Walks of every length preserve expectation zero.

theorem Cslib.RotationMap.expect_mul_walk_comm {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] (f g : V → ℝ) : (Finset.univ.expect fun (v : V) => f v * G.walk g v) = Finset.univ.expect fun (v : V) => G.walk f v * g v

The walk operator is self-adjoint for the uniform inner product.

theorem Cslib.RotationMap.expect_walk_sq_le {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] (f : V → ℝ) : (Finset.univ.expect fun (v : V) => G.walk f v ^ 2) ≤ Finset.univ.expect fun (v : V) => f v ^ 2

The walk operator does not increase the second moment.

noncomputable def Cslib.RotationMap.spectralExpansion {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] : ℝ

The spectral expansion λ(G): the operator norm, for the Euclidean norm, of the walk operator on the functions orthogonal to the constants Arora and Barak, Section 21.1. As the walk operator is self-adjoint, this is the largest absolute value of its eigenvalues on those functions, but nothing here depends on that: λ(G) is used through its characterization spectralExpansion_le_iff.

theorem Cslib.RotationMap.spectralExpansion_nonneg {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] : 0 ≤ G.spectralExpansion

The spectral expansion is nonnegative.

theorem Cslib.RotationMap.expect_walk_sq_le_spectralExpansion_sq_mul {V : Type u_1} {D : Type u_2} {G : RotationMap V D} [Fintype V] [Fintype D] {f : V → ℝ} (hf : (Finset.univ.expect fun (v : V) => f v) = 0) : (Finset.univ.expect fun (v : V) => G.walk f v ^ 2) ≤ G.spectralExpansion ^ 2 * Finset.univ.expect fun (v : V) => f v ^ 2

On functions of expectation zero, the walk operator multiplies the second moment by at most λ(G) ^ 2.

theorem Cslib.RotationMap.spectralExpansion_le {V : Type u_1} {D : Type u_2} {G : RotationMap V D} [Fintype V] [Fintype D] {c : ℝ} (hc : 0 ≤ c) (h : ∀ (f : V → ℝ), (Finset.univ.expect fun (v : V) => f v) = 0 → (Finset.univ.expect fun (v : V) => G.walk f v ^ 2) ≤ c ^ 2 * Finset.univ.expect fun (v : V) => f v ^ 2) : G.spectralExpansion ≤ c

If the walk operator multiplies the second moment of every function of expectation zero by at most c ^ 2, where c ≥ 0, then λ(G) ≤ c.

theorem Cslib.RotationMap.spectralExpansion_le_iff {V : Type u_1} {D : Type u_2} {G : RotationMap V D} [Fintype V] [Fintype D] {c : ℝ} (hc : 0 ≤ c) : G.spectralExpansion ≤ c ↔ ∀ (f : V → ℝ), (Finset.univ.expect fun (v : V) => f v) = 0 → (Finset.univ.expect fun (v : V) => G.walk f v ^ 2) ≤ c ^ 2 * Finset.univ.expect fun (v : V) => f v ^ 2

λ(G) ≤ c, for c ≥ 0, exactly when the walk operator multiplies the second moment of every function of expectation zero by at most c ^ 2.

theorem Cslib.RotationMap.spectralExpansion_le_one {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] : G.spectralExpansion ≤ 1

The spectral expansion is at most one.

theorem Cslib.RotationMap.expect_walk_pow_sq_le_spectralExpansion_pow_mul {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] {f : V → ℝ} (hf : (Finset.univ.expect fun (v : V) => f v) = 0) (t : ℕ) : (Finset.univ.expect fun (v : V) => (G.walk ^ t) f v ^ 2) ≤ G.spectralExpansion ^ (2 * t) * Finset.univ.expect fun (v : V) => f v ^ 2

Walks of length t multiply the second moment of a function of expectation zero by at most λ(G) ^ (2 t).

theorem Cslib.RotationMap.spectralExpansion_eq_zero_of_subsingleton {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] [Subsingleton V] : G.spectralExpansion = 0

On at most one vertex the spectral expansion is zero: the only function of expectation zero is zero.

theorem Cslib.RotationMap.spectralExpansion_eq_of_walk_eq {V : Type u_1} {D : Type u_2} {G : RotationMap V D} [Fintype V] [Fintype D] {E : Type u_3} [Fintype E] {H : RotationMap V E} (h : G.walk = H.walk) : G.spectralExpansion = H.spectralExpansion

Two regular multigraphs on the same vertices with the same walk operator have the same spectral expansion, whatever their edge labels.