A base graph for the zig-zag tower

The zig-zag tower Cslib.RotationMap.zigzagTower is built from one D-regular base graph on |D| ^ 4 vertices, named by Fin 2 → D × D, of spectral expansion at most 1 / 5. Reingold, Vadhan and Wigderson find it by exhaustive search, its existence being known from probabilistic arguments, or construct it algebraically Reingold, Vadhan and Wigderson, Section 5. Here it is obtained from the non-explicit family Cslib.RotationMap.expander by powering.

The family provides a 120-regular multigraph of spectral expansion at most 1 - 1 / 360000 on every finite type, so the base can live directly on the type it must have: with D = Fin t → Fin 120, the labels of the t-th power of a 120-regular multigraph, the t-th power Cslib.RotationMap.zigzagTowerBase t of expander (Fin 2 → D × D) is a D-regular multigraph on Fin 2 → D × D of spectral expansion at most (1 - 1 / 360000) ^ t, which is at most 1 / 5 once t ≥ 1440000, as (1 - x) ^ t (1 + t x) ≤ 1.

The zig-zag tower over this base is a family of 120 ^ (2 t)-regular multigraphs on 120 ^ (4 t (n + 1)) vertices, n ∈ ℕ, of spectral expansion at most 2 / 5 (Cslib.RotationMap.exists_spectralExpansion_zigzagTower_le). The base graph is its only non-explicit ingredient: the tower is computed from the rotation map of the base by a recursion without choices, while the base is expander, chosen by a counting argument.

Main definitions

• Cslib.RotationMap.zigzagTowerBase: the t-th power of expander (Fin 2 → D × D), where D = Fin t → Fin 120.

Main results

• Cslib.RotationMap.spectralExpansion_zigzagTowerBase_le_one_div_five: for t ≥ 1440000, the base graph has spectral expansion at most 1 / 5.
• Cslib.RotationMap.spectralExpansion_zigzagTower_zigzagTowerBase_le, Cslib.RotationMap.card_zigzagTowerVertex_zigzagTowerBase: the tower over it consists of 120 ^ (2 t)-regular multigraphs on 120 ^ (4 t (n + 1)) vertices of spectral expansion at most 2 / 5.
• Cslib.RotationMap.exists_spectralExpansion_zigzagTower_le: constant-degree expanders on d ^ (4 (n + 1)) vertices for every n, explicit given one base graph.

References

• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications

noncomputable def Cslib.RotationMap.zigzagTowerBase (t : ℕ) : RotationMap (Fin 2 → (Fin t → Fin 120) × (Fin t → Fin 120)) (Fin t → Fin 120)

A base graph for the zig-zag tower: the t-th power of the 120-regular multigraph expander on Fin 2 → D × D, where D = Fin t → Fin 120 are the labels of the power. It is D-regular on |D| ^ 4 vertices, and its spectral expansion is at most 1 / 5 for t ≥ 1440000 (spectralExpansion_zigzagTowerBase_le_one_div_five).

theorem Cslib.RotationMap.spectralExpansion_zigzagTowerBase_le (t : ℕ) : (zigzagTowerBase t).spectralExpansion ≤ (1 - 1 / 360000) ^ t

The spectral expansion of the base graph is at most (1 - 1 / 360000) ^ t.

theorem Cslib.RotationMap.spectralExpansion_zigzagTowerBase_le_one_div_five {t : ℕ} (ht : 1440000 ≤ t) : (zigzagTowerBase t).spectralExpansion ≤ 1 / 5

For t ≥ 1440000, the spectral expansion of the base graph is at most 1 / 5.

theorem Cslib.RotationMap.card_zigzagTowerVertex_zigzagTowerBase (t n : ℕ) : Fintype.card (ZigzagTowerVertex (Fin 2 → (Fin t → Fin 120) × (Fin t → Fin 120)) n) = 120 ^ (4 * t * (n + 1))

The graphs of the zig-zag tower over zigzagTowerBase t have 120 ^ (4 t (n + 1)) vertices.

theorem Cslib.RotationMap.spectralExpansion_zigzagTower_zigzagTowerBase_le {t : ℕ} (ht : 1440000 ≤ t) (n : ℕ) : ((zigzagTowerBase t).zigzagTower (Equiv.refl (Fin 2 → (Fin t → Fin 120) × (Fin t → Fin 120))) n).spectralExpansion ≤ 2 / 5

Expanders from the zig-zag product Reingold, Vadhan and Wigderson, Theorem 1.4: for t ≥ 1440000, the graphs of the zig-zag tower over zigzagTowerBase t, which are 120 ^ (2 t)-regular on 120 ^ (4 t (n + 1)) vertices, have spectral expansion at most 2 / 5.

theorem Cslib.RotationMap.exists_spectralExpansion_zigzagTower_le : ∃ (D : Type) (x : Fintype D) (H : RotationMap (Fin 2 → D × D) D), 1 < Fintype.card D ∧ H.spectralExpansion ≤ 1 / 5 ∧ ∀ (n : ℕ), Fintype.card (ZigzagTowerVertex (Fin 2 → D × D) n) = Fintype.card D ^ (4 * (n + 1)) ∧ (H.zigzagTower (Equiv.refl (Fin 2 → D × D)) n).spectralExpansion ≤ 2 / 5

Constant-degree expanders on d ^ (4 (n + 1)) vertices, explicit given one base graph Reingold, Vadhan and Wigderson, Theorem 1.4 Hoory, Linial and Wigderson, Section 9.2: there are a finite type D of at least two labels and a D-regular multigraph H on Fin 2 → D × D of spectral expansion at most 1 / 5 such that, for every n, the zig-zag tower zigzagTower H _ n is a |D| ^ 2-regular multigraph on |D| ^ (4 (n + 1)) vertices of spectral expansion at most 2 / 5.

The tower is explicit given H: zigzagTower computes its rotation maps from that of H by a recursion without choices. Only H is obtained non-constructively, as zigzagTowerBase 1440000.