Reingold's transformation

Reingold's algorithm for undirected connectivity Reingold Arora and Barak, Section 21.4 turns a regular graph into one in which every connected component is an expander of constant degree, without merging components, by alternating the zig-zag product with a fixed small expander H and squaring.

Let H be a regular multigraph on B with labels E, together with an equivalence e : B ≃ (Fin 2 → E × E), so that H has |E| ^ 4 vertices and degree |E|. For a B-regular graph G on V, the zig-zag product G ⓩ H is E × E-regular on V × B, and its square is Fin 2 → E × E-regular, so e.symm renames its labels back to B:

reingoldStep H e G = ((G ⓩ H) ^ 2).relabel e.symm,

a B-regular graph on V × B. Starting from G₀ = G, reingold H e G ℓ is the graph G_ℓ = reingoldStep H e G_{ℓ - 1}, on the vertices ReingoldVertex V B ℓ = (⋯ (V × B) × ⋯) × B. Each vertex of G_ℓ lies over a vertex of G, its root.

Spectral gap. By the zig-zag theorem λ(G ⓩ H) ≤ 1 - (1 - λ(G)) (1 - λ(H)) ^ 2, so with λ(H) ≤ 1 / 5 a gap γ = 1 - λ(G) becomes at least 1 - (1 - 16 γ / 25) ^ 2 (spectralExpansion_reingoldStep_le), which is at least min (6 γ / 5) (1 / 5) (min_le_one_sub_spectralExpansion_reingoldStep). After ℓ steps the gap is at least min ((6 / 5) ^ ℓ γ) (1 / 5) (min_pow_le_one_sub_spectralExpansion_reingold). Reingold takes the eighth power of G ⓩ H, for a D-regular base graph on D ^ 16 vertices with λ(H) ≤ 1 / 2, and obtains λ ↦ max (λ ^ 2) (1 / 2) in the proof of Reingold, Lemma 3.2; taking the square, with the base graph of the zig-zag tower, the gap grows by the factor 6 / 5 instead, which changes only the constant in the number of steps.

Components. The transformation is natural for homomorphisms (Cslib.RotationMap.Hom.reingold), so it acts separately on each connected component Reingold, Lemma 3.3: the transform of the connected component of s maps into the transform of G, onto the vertices over that component. A walk in G_ℓ stays over one component of G (reachable_root_neighbor_pow_reingold). If at least half of the edges at every vertex of G are self-loops, a connected component on N ≤ |V| vertices has spectral gap at least 1 / (2 N² |B|²), so once 2 |V|² |B|² 5 ^ ℓ ≤ 5 · 6 ^ ℓ the transform of every component is an expander with λ ≤ 4 / 5, on at most |V| |B| ^ ℓ vertices. Walks of length T then reach every vertex over the component as soon as |V| |B| ^ ℓ 4 ^ T ≤ 5 ^ T (exists_neighbor_pow_reingold_eq). Hence (reachable_iff_exists_root_neighbor_pow_reingold): t is reachable from s in G exactly when some walk of length T in G_ℓ from a vertex over s ends over t. Both ℓ and T are O(log |V|) when |B| is a constant.

Main definitions

• Cslib.RotationMap.reingoldStep: one step ((G ⓩ H) ^ 2).relabel e.symm of the transformation.
• Cslib.RotationMap.reingold: the graphs G_ℓ, on the iterated products Cslib.RotationMap.ReingoldVertex V B ℓ.

Main results

• Cslib.RotationMap.min_le_one_sub_spectralExpansion_reingoldStep, Cslib.RotationMap.min_pow_le_one_sub_spectralExpansion_reingold: the spectral gap grows geometrically until it reaches 1 / 5.
• Cslib.RotationMap.reachable_root_neighbor_pow_reingold: walks in G_ℓ stay over a connected component of G.
• Cslib.RotationMap.exists_neighbor_pow_reingold_eq: short walks in G_ℓ reach every vertex over the connected component of the start.
• Cslib.RotationMap.reachable_iff_exists_root_neighbor_pow_reingold: connectivity in G is decided by the walks of length T in G_ℓ from one vertex.

References

• O. Reingold, Undirected connectivity in log-space
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders

def Cslib.RotationMap.reingoldStep {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u_2} (G : RotationMap V B) : RotationMap (V × B) B

One step of Reingold's transformation, a variant of Reingold, Definition 3.1 Arora and Barak, Section 21.4 with the square instead of the eighth power: the square of the zig-zag product of a B-regular graph G with the graph H on B, whose labels Fin 2 → E × E are renamed back to B by e.symm.

def Cslib.RotationMap.reingold {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u} (G : RotationMap V B) (ℓ : ℕ) : RotationMap (ReingoldVertex V B ℓ) B

Reingold's transformation, a variant of Reingold, Definition 3.1 with the square instead of the eighth power: reingold H e G ℓ is the graph G_ℓ obtained from G₀ = G by ℓ steps G_{i + 1} = ((G_i ⓩ H) ^ 2).relabel e.symm.

@[simp]

theorem Cslib.RotationMap.reingold_zero {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u} (G : RotationMap V B) : H.reingold e G 0 = G

The graph G₀ is the original graph.

theorem Cslib.RotationMap.reingold_succ {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u} (G : RotationMap V B) (ℓ : ℕ) : H.reingold e G (ℓ + 1) = H.reingoldStep e (H.reingold e G ℓ)

Each graph of the transformation is a step of the transformation from the previous one.

def Cslib.RotationMap.Hom.reingold {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V W : Type u} {G : RotationMap V B} {G' : RotationMap W B} (φ : G.Hom G') (ℓ : ℕ) : (H.reingold e G ℓ).Hom (H.reingold e G' ℓ)

Reingold's transformation is natural: a homomorphism of graphs induces homomorphisms of their transforms, acting on the roots.

theorem Cslib.RotationMap.Hom.reingold_apply {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V W : Type u} {G : RotationMap V B} {G' : RotationMap W B} (φ : G.Hom G') (ℓ : ℕ) (x : ReingoldVertex V B ℓ) : (reingold H e φ ℓ) x = ReingoldVertex.map (⇑φ) ℓ x

The homomorphism of the transforms applies the homomorphism to the root.

theorem Cslib.RotationMap.reachable_root_neighbor_pow_reingold {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) {V : Type u} (G : RotationMap V B) (ℓ T : ℕ) (x : ReingoldVertex V B ℓ) (k : Fin T → B) : G.toSimpleGraph.Reachable x.root (((H.reingold e G ℓ).pow T).neighbor x k).root

Walks in G_ℓ stay over a connected component of G: the walk of length T from any vertex of G_ℓ ends over a vertex reachable in G from the root of the start.

theorem Cslib.RotationMap.spectralExpansion_reingoldStep_le {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) [Fintype B] [Fintype E] {V : Type u_2} [Fintype V] (G : RotationMap V B) : (H.reingoldStep e G).spectralExpansion ≤ (1 - (1 - G.spectralExpansion) * (1 - H.spectralExpansion) ^ 2) ^ 2

One step of the transformation turns the spectral gap 1 - λ(G) into at least 1 - (1 - (1 - λ(G)) (1 - λ(H)) ^ 2) ^ 2, by the zig-zag theorem.

theorem Cslib.RotationMap.min_le_one_sub_spectralExpansion_reingoldStep {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) [Fintype B] [Fintype E] {V : Type u_2} [Fintype V] (hH : H.spectralExpansion ≤ 1 / 5) (G : RotationMap V B) {γ : ℝ} (hγ₀ : 0 ≤ γ) (hγ : γ ≤ 1 - G.spectralExpansion) : min (6 / 5 * γ) (1 / 5) ≤ 1 - (H.reingoldStep e G).spectralExpansion

The spectral gap grows, as in the proof of Reingold, Lemma 3.2: if λ(H) ≤ 1 / 5 and the spectral gap of G is at least γ ≥ 0, one step of the transformation has spectral gap at least min (6 γ / 5) (1 / 5).

theorem Cslib.RotationMap.min_pow_le_one_sub_spectralExpansion_reingold {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) [Fintype B] [Fintype E] {V : Type u} [Fintype V] (hH : H.spectralExpansion ≤ 1 / 5) (G : RotationMap V B) {γ : ℝ} (hγ₀ : 0 ≤ γ) (hγ : γ ≤ 1 - G.spectralExpansion) (ℓ : ℕ) : min ((6 / 5) ^ ℓ * γ) (1 / 5) ≤ 1 - (H.reingold e G ℓ).spectralExpansion

The spectral gap grows geometrically Reingold, Lemma 3.2: if λ(H) ≤ 1 / 5 and the spectral gap of G is at least γ ≥ 0, the ℓ-th graph of the transformation has spectral gap at least min ((6 / 5) ^ ℓ γ) (1 / 5).

theorem Cslib.RotationMap.exists_neighbor_pow_reingold_eq {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) [Fintype B] [Fintype E] [Nonempty B] {V : Type u} [Fintype V] [DecidableEq V] (hH : H.spectralExpansion ≤ 1 / 5) (G : RotationMap V B) (hG : ∀ (v : V), Fintype.card B ≤ 2 * {i : B | G.neighbor v i = v}.card) {ℓ T : ℕ} (hℓ : 2 * Fintype.card V ^ 2 * Fintype.card B ^ 2 * 5 ^ ℓ ≤ 5 * 6 ^ ℓ) (hT : Fintype.card V * Fintype.card B ^ ℓ * 4 ^ T ≤ 5 ^ T) {x y : ReingoldVertex V B ℓ} (hxy : G.toSimpleGraph.Reachable x.root y.root) : ∃ (k : Fin T → B), ((H.reingold e G ℓ).pow T).neighbor x k = y

Short walks in G_ℓ reach the whole component Reingold, Lemmas 3.2 and 3.3 and Proposition 2.2: if λ(H) ≤ 1 / 5, at least half of the edges at every vertex of G are self-loops, 2 |V|² |B|² 5 ^ ℓ ≤ 5 · 6 ^ ℓ and |V| |B| ^ ℓ 4 ^ T ≤ 5 ^ T, then for any two vertices x and y of G_ℓ over vertices reachable from each other in G, some walk of length exactly T leads from x to y. The transform of the connected component of the root of x is an expander with λ ≤ 4 / 5 on at most |V| |B| ^ ℓ vertices, and it maps into G_ℓ.

theorem Cslib.RotationMap.reachable_iff_exists_root_neighbor_pow_reingold {B : Type u} {E : Type u_1} (H : RotationMap B E) (e : B ≃ (Fin 2 → E × E)) [Fintype B] [Fintype E] [Nonempty B] {V : Type u} [Fintype V] [DecidableEq V] (hH : H.spectralExpansion ≤ 1 / 5) (G : RotationMap V B) (hG : ∀ (v : V), Fintype.card B ≤ 2 * {i : B | G.neighbor v i = v}.card) {ℓ T : ℕ} (hℓ : 2 * Fintype.card V ^ 2 * Fintype.card B ^ 2 * 5 ^ ℓ ≤ 5 * 6 ^ ℓ) (hT : Fintype.card V * Fintype.card B ^ ℓ * 4 ^ T ≤ 5 ^ T) (s t : V) (b : B) : G.toSimpleGraph.Reachable s t ↔ ∃ (k : Fin T → B), (((H.reingold e G ℓ).pow T).neighbor (ReingoldVertex.mk s b ℓ) k).root = t

Undirected connectivity by short walks in Reingold's transform Reingold Arora and Barak, Section 21.4: if λ(H) ≤ 1 / 5, at least half of the edges at every vertex of G are self-loops, 2 |V|² |B|² 5 ^ ℓ ≤ 5 · 6 ^ ℓ and |V| |B| ^ ℓ 4 ^ T ≤ 5 ^ T, then t is reachable from s in G exactly when some walk of length T in G_ℓ from the vertex (⋯ (s, b) ⋯, b) ends over t.