A base graph for the tower exists #

The zig-zag tower is seeded by a single finite graph whose vertices number the fourth power of its degree and whose spectral bound is a fifth. Such a graph is what Reingold, Vadhan and Wigderson find by exhaustive search; here it comes from any expander family at all, by raising one member to a power.

Powering leaves the vertex set alone and raises both the degree and the bound to the same power, so taking the member on degree ^ (4 * m) vertices and powering it m times gives degree ^ (4 * m) = (degree ^ m) ^ 4 vertices against degree degree ^ m — and lam ^ m ≤ 1 / 5 once m is large enough.

Applied to randExpander, this shows a ZigZagBase exists.

Main definitions #

Complexity.ExpanderFamily.fifthExp — a power taking the bound below a fifth
Complexity.ExpanderFamily.toZigZagBase — the base graph

Main results #

Complexity.nonempty_zigZagBase — a base graph exists

source

theorem Complexity.ExpanderFamily.exists_pow_le_fifth (E : ExpanderFamily) :

∃ (m : ℕ), E.lam ^ m ≤ 1 / 5

source

noncomputable def Complexity.ExpanderFamily.fifthExp (E : ExpanderFamily) :

ℕ

A power taking the family's bound to at most a fifth.

Equations

E.fifthExp = Classical.choose ⋯

Instances For

source

theorem Complexity.ExpanderFamily.pow_fifthExp_le (E : ExpanderFamily) :

E.lam ^ E.fifthExp ≤ 1 / 5

source

noncomputable def Complexity.ExpanderFamily.baseOrder (E : ExpanderFamily) :

ℕ

The size at which the powered member has as many vertices as the fourth power of its degree.

Equations

E.baseOrder = E.degree ^ (4 * E.fifthExp)

Instances For

source

noncomputable def Complexity.ExpanderFamily.toZigZagBase (E : ExpanderFamily) :

ZigZagBase

A base for the zig-zag tower.

Equations

E.toZigZagBase = { base := (E.graph E.baseOrder).power E.fifthExp, card_eq := ⋯, lam := E.lam ^ E.fifthExp, lam_nonneg := ⋯, lam_le := ⋯, spectral := ⋯ }