The pieces a merge is built from

Explicit expander constructions come in special sizes — squares, powers — but ExpanderFamily wants a member on every n. An expander on N vertices is folded onto n of them by identifying u with u mod n, with self-loops padding the fibres that come up short. MergeGen carries out that fold at an arbitrary width; this module holds the two ingredients it rests on.

The first is the estimate on the old steps. Write f for a function on the merged graph and F = f ∘ π for its lift. Splitting F into its mean and its centred part and applying the base's spectral bound to the latter gives λ² ‖F‖² + (1 - λ²) N c², where c is the mean of F — nonzero, because the heavier fibres weigh more.

The second is that the fibres stay balanced: with (m - 1) n ≤ N at most one of a vertex's m slots is empty, so however large the width, the padding costs one loop per vertex.

Main definitions

• Complexity.RegGraph.proj — the new vertex an old one lands on
• Complexity.RegGraph.liftN — the old vertex in a given slot of a fibre

Main results

• Complexity.RegGraph.sum_sq_step_lift_le — the old steps, with the mean corrected
• Complexity.RegGraph.card_liftN_none_le_one — the balanced fibres a general merge needs

The fibres of a merge

def Complexity.RegGraph.proj {N : ℕ} (n : ℕ) (hn : 0 < n) (u : Fin N) : Fin n

The new vertex an old vertex lands on.

Equations

• Complexity.RegGraph.proj n hn u = ⟨↑u % n, ⋯⟩

The spectral bound

@[reducible, inline]

abbrev Complexity.RegGraph.base {N d : ℕ} (hd : 0 < d) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) : RegGraph

The base graph, on Fin N.

Equations

• Complexity.RegGraph.base hd rot hrot = Complexity.RegGraph.ofRot d hd N rot hrot

theorem Complexity.RegGraph.sum_sq_step_lift_le {N d n : ℕ} (hn : 0 < n) (hd : 0 < d) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) {lam : ℝ} (hspec : (base hd rot hrot).SpectralBound lam) (hN0 : 0 < N) (f : Fin n → ℝ) : ∑ u : Fin N, (base hd rot hrot).step (fun (w : (base hd rot hrot).V) => f (proj n hn w)) u ^ 2 ≤ lam ^ 2 * ∑ u : Fin N, f (proj n hn u) ^ 2 + (1 - lam ^ 2) * ((∑ u : Fin N, f (proj n hn u)) ^ 2 / ↑N)

The old steps of the lift, with the mean corrected.

Balanced fibres, for a merge of any width

With (m - 1) n ≤ N ≤ m n every fibre has m - 1 or m elements, so at most one of the m slots is empty and the padding costs one loop per vertex however large m is.

These are the two facts a general merge rests on; they are stated for a natural-number slot index, which is the form the general construction needs.

def Complexity.RegGraph.liftN (N n : ℕ) (v : Fin n) (i : ℕ) : Option (Fin N)

The old vertex in slot i of the fibre over v, if there is one.

Equations

• Complexity.RegGraph.liftN N n v i = if h : ↑v + i * n < N then some ⟨↑v + i * n, h⟩ else none

theorem Complexity.RegGraph.liftN_isSome {N n m : ℕ} (hm : (m - 1) * n ≤ N) (v : Fin n) {i : ℕ} (hi : i + 1 < m) : (liftN N n v i).isSome = true

Every slot but the last is filled, when (m - 1) n ≤ N.

theorem Complexity.RegGraph.card_liftN_none_le_one {N n m : ℕ} (hm : (m - 1) * n ≤ N) (v : Fin n) : {i ∈ Finset.range m | liftN N n v i = none}.card ≤ 1

So at most one slot is empty.