Connectivity and spectral expansion

Two facts connect the spectral expansion λ(G) of a regular multigraph with its connectivity, and they are the two ends of Reingold's algorithm for undirected connectivity Reingold Arora and Barak, Section 21.4.

A connected graph has a spectral gap. If G is connected, a set S of at most half of the vertices has an edge leaving it, so the edge expansion of G is at least 1 / |V|, and Cheeger's inequality bounds the second eigenvalue of the walk operator by 1 - 1 / (2 |V|² |D|²). When at least half of the edges at every vertex are self-loops, the walk operator is positive semidefinite (expect_mul_walk_nonneg), so this also bounds λ(G) (spectralExpansion_le_of_preconnected). Reingold uses the sharper bound 1 - 1 / (D N²) for connected nonbipartite graphs, due to Alon and Sudakov Reingold, Lemma 2.5; any inverse polynomial gap suffices for his algorithm. Self-loops are often added for this purpose by passing to the lazy graph (Cslib.RotationMap.lazy), whose spectral expansion edge expansion bounds in the same way (Cslib.RotationMap.spectralExpansion_lazy_le_of_mul_card_le_card_interedges_compl); the bound here applies to any graph that already has enough self-loops, without relabelling.

In a good expander, short walks reach every vertex. If λ(G) ^ t (|V| - 1) < 1, then for any two vertices u and v some walk of length exactly t leads from u to v (exists_neighbor_pow_eq): by the mixing lemma, a random walk of length t from u ends at v with probability at least (1 - λ(G) ^ t (|V| - 1)) / |V| > 0. So an expander with λ(G) ≤ c < 1 has diameter O(log |V|); Reingold derives this from vertex expansion instead Reingold, Proposition 2.2.

Main results

• Cslib.RotationMap.interedges_compl_nonempty: in a connected graph, an edge leaves every nonempty proper set of vertices.
• Cslib.RotationMap.expect_mul_walk_nonneg: if at least half of the edges at every vertex are self-loops, the walk operator is positive semidefinite.
• Cslib.RotationMap.spectralExpansion_le_of_preconnected: a connected graph with at least half self-loops at every vertex has λ(G) ≤ 1 - 1 / (2 |V|² |D|²).
• Cslib.RotationMap.exists_neighbor_pow_eq: if λ(G) ^ t (|V| - 1) < 1, every vertex is reachable from every other by a walk of length exactly t.

References

• O. Reingold, Undirected connectivity in log-space
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications

theorem Cslib.RotationMap.interedges_compl_nonempty {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [DecidableEq V] [Fintype D] (hG : G.toSimpleGraph.Preconnected) {S : Finset V} (hS : S.Nonempty) (hS' : S ≠ Finset.univ) : (G.interedges S Sᶜ).Nonempty

In a connected graph, some edge leaves every nonempty proper set of vertices.

theorem Cslib.RotationMap.expect_mul_walk_nonneg {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [DecidableEq V] [Fintype D] (hG : ∀ (v : V), Fintype.card D ≤ 2 * {i : D | G.neighbor v i = v}.card) (f : V → ℝ) : 0 ≤ Finset.univ.expect fun (v : V) => f v * G.walk f v

If at least half of the edges at every vertex are self-loops, the walk operator is positive semidefinite: 0 ≤ 𝔼 v, f v * G.walk f v for every f.

theorem Cslib.RotationMap.spectralExpansion_le_of_preconnected {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [DecidableEq V] [Fintype D] (hloop : ∀ (v : V), Fintype.card D ≤ 2 * {i : D | G.neighbor v i = v}.card) (hconn : G.toSimpleGraph.Preconnected) : G.spectralExpansion ≤ 1 - 1 / (2 * ↑(Fintype.card V) ^ 2 * ↑(Fintype.card D) ^ 2)

A connected graph has a spectral gap. If G is connected and at least half of the edges at every vertex are self-loops, then λ(G) ≤ 1 - 1 / (2 |V|² |D|²): an edge leaves every set of at most half of the vertices, which bounds the second eigenvalue by Cheeger's inequality Hoory, Linial and Wigderson, Theorem 2.4, and the self-loops make the walk operator positive semidefinite, so that the second eigenvalue is λ(G). Compare the lazy graph, whose walk is positive semidefinite by construction (spectralExpansion_lazy_le_of_mul_card_le_card_interedges_compl).

theorem Cslib.RotationMap.exists_neighbor_pow_eq {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] [Nonempty D] {t : ℕ} (h : G.spectralExpansion ^ t * (↑(Fintype.card V) - 1) < 1) (u v : V) : ∃ (k : Fin t → D), (G.pow t).neighbor u k = v

Short walks in an expander reach every vertex. If λ(G) ^ t (|V| - 1) < 1, then from every vertex u some walk of length exactly t leads to any given vertex v: by the mixing lemma, a uniformly random walk of length t from u ends at v with probability at least (1 - λ(G) ^ t (|V| - 1)) / |V|.