Merging at an arbitrary width

ExpanderMerge folds N ≤ 3 n vertices onto n. The zig-zag tower produces sizes far more widely spaced than that, so the fold has to work at any width: N vertices onto n, with (m - 1) n ≤ N ≤ m n.

What keeps the estimate under control at every width is that the fibres stay balanced — ExpanderMerge.card_liftN_none_le_one — so however large m is, each new vertex needs at most one padding loop.

This module carries the combinatorial layer: the rotation map and the graph.

Main definitions

• Complexity.RegGraph.mergeRotN — the rotation map of the wide merge
• Complexity.RegGraph.mergedN — the merged graph

Main results

• Complexity.RegGraph.mergeRotN_involutive
• Complexity.RegGraph.order_mergedN, Complexity.RegGraph.deg_mergedN
• Complexity.RegGraph.step_mergedN — the merged walk averages the m slots
• Complexity.RegGraph.sq_step_mergedN_le — and Jensen bounds its square
• Complexity.RegGraph.sum_over_liftN — the filled slots enumerate the old vertices
• Complexity.RegGraph.sum_sq_termN_le — the split into old steps and padding
• Complexity.RegGraph.spectralBound_mergedN — the spectral bound at any width
• Complexity.mergeWidth — a width that always works

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

The new vertex an old one folds onto.

Equations

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

def Complexity.RegGraph.slotN {N : ℕ} (n m : ℕ) (hN : N ≤ m * n) (u : Fin N) : Fin m

Which slot of its fibre an old vertex occupies.

Equations

• Complexity.RegGraph.slotN n m hN u = ⟨↑u / n, ⋯⟩

theorem Complexity.RegGraph.liftN_projN_slotN {N n m : ℕ} (hn : 0 < n) (hN : N ≤ m * n) (u : Fin N) : liftN N n (projN n hn u) ↑(slotN n m hN u) = some u

theorem Complexity.RegGraph.projN_liftN {N n : ℕ} (hn : 0 < n) (v : Fin n) (i : ℕ) (u : Fin N) (h : liftN N n v i = some u) : projN n hn u = v

theorem Complexity.RegGraph.slotN_liftN {N n m : ℕ} (hn : 0 < n) (hN : N ≤ m * n) (v : Fin n) (i : ℕ) (u : Fin N) (h : liftN N n v i = some u) : ↑(slotN n m hN u) = i

def Complexity.RegGraph.mergeRotN {N d n m : ℕ} (hn : 0 < n) (hN : N ≤ m * n) (rot : Fin N × Fin d → Fin N × Fin d) (x : Fin n × Fin m × Fin d) : Fin n × Fin m × Fin d

The rotation map of the wide merge.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RegGraph.mergeRotN_involutive {N d n m : ℕ} (hn : 0 < n) (hN : N ≤ m * n) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) : Function.Involutive (mergeRotN hn hN rot)

def Complexity.RegGraph.mergedN {N d n m : ℕ} (hn : 0 < n) (hd : 0 < d) (hm : 0 < m) (hN : N ≤ m * n) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) : RegGraph

The wide merge.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.RegGraph.order_mergedN {N d n m : ℕ} (hn : 0 < n) (hd : 0 < d) (hm : 0 < m) (hN : N ≤ m * n) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) : (mergedN hn hd hm hN rot hrot).order = n

@[simp]

theorem Complexity.RegGraph.deg_mergedN {N d n m : ℕ} (hn : 0 < n) (hd : 0 < d) (hm : 0 < m) (hN : N ≤ m * n) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) : (mergedN hn hd hm hN rot hrot).deg = m * d

The walk of the wide merge

noncomputable def Complexity.RegGraph.termN {N d n : ℕ} (hn : 0 < n) (hd : 0 < d) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) (f : Fin n → ℝ) (v : Fin n) (i : ℕ) : ℝ

A term of the merged step at v: the old step at the vertex in slot i, or f v where the slot is empty.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RegGraph.step_mergedN {N d n m : ℕ} (hn : 0 < n) (hd : 0 < d) (hm : 0 < m) (hN : N ≤ m * n) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) (f : Fin n → ℝ) (v : Fin n) : (mergedN hn hd hm hN rot hrot).step f v = (∑ i ∈ Finset.range m, termN hn hd rot hrot f v i) / ↑m

The merged walk is the average over the slots.

theorem Complexity.RegGraph.sq_step_mergedN_le {N d n m : ℕ} (hn : 0 < n) (hd : 0 < d) (hm : 0 < m) (hN : N ≤ m * n) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) (f : Fin n → ℝ) (v : Fin n) : (mergedN hn hd hm hN rot hrot).step f v ^ 2 ≤ (∑ i ∈ Finset.range m, termN hn hd rot hrot f v i ^ 2) / ↑m

Jensen: the square of the average is at most the average of the squares.

Summing over the slots

theorem Complexity.RegGraph.sum_over_liftN {N n m : ℕ} (hn : 0 < n) (hN : N ≤ m * n) (g : Fin N → ℝ) : (∑ p : Fin n × Fin m, match liftN N n p.1 ↑p.2 with | some u => g u | none => 0) = ∑ u : Fin N, g u

The filled slots are exactly the old vertices.

theorem Complexity.RegGraph.sum_sq_termN_le {N d n m : ℕ} (hn : 0 < n) (hd : 0 < d) (hN : N ≤ m * n) (hm1 : (m - 1) * n ≤ N) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) (f : Fin n → ℝ) : ∑ v : Fin n, ∑ i : Fin m, termN hn hd rot hrot f v ↑i ^ 2 ≤ ∑ u : Fin N, (base hd rot hrot).step (fun (w : (base hd rot hrot).V) => f (projN n hn w)) u ^ 2 + ∑ v : Fin n, f v ^ 2

Splitting the slot terms: the old steps, plus at most one padding per vertex — this is where balance of the fibres is used.

The spectral bound at any width

theorem Complexity.RegGraph.projN_eq_proj {N n : ℕ} (hn : 0 < n) : projN n hn = proj n hn

The wide projection is the one ExpanderMerge already used.

theorem Complexity.RegGraph.sum_sq_liftN_le {N n m : ℕ} (hn : 0 < n) (hN : N ≤ m * n) (f : Fin n → ℝ) : ∑ u : Fin N, f (projN n hn u) ^ 2 ≤ ↑m * ∑ v : Fin n, f v ^ 2

theorem Complexity.RegGraph.sum_liftN_eq {N n m : ℕ} (hn : 0 < n) (hN : N ≤ m * n) (hm1 : (m - 1) * n ≤ N) (hm : 0 < m) (f : Fin n → ℝ) (hf : ∑ v : Fin n, f v = 0) : ∑ u : Fin N, f (projN n hn u) = ∑ v : Fin n, match liftN N n v (m - 1) with | some val => f v | none => 0

The lift's total, for a mean-zero f: only the last slot survives.

theorem Complexity.RegGraph.sq_sum_liftN_le {N n m : ℕ} (hn : 0 < n) (hN : N ≤ m * n) (hm1 : (m - 1) * n ≤ N) (hm : 0 < m) (f : Fin n → ℝ) (hf : ∑ v : Fin n, f v = 0) : (∑ u : Fin N, f (projN n hn u)) ^ 2 ≤ ↑n * ∑ v : Fin n, f v ^ 2

The mean of the lift is small.

theorem Complexity.RegGraph.spectralBound_mergedN {N d n m : ℕ} (hn : 0 < n) (hd : 0 < d) (hm : 0 < m) (hN : N ≤ m * n) (hm1 : (m - 1) * n ≤ N) (h2 : 2 * n ≤ N) (rot : Fin N × Fin d → Fin N × Fin d) (hrot : Function.Involutive rot) {lam : ℝ} (hlam : lam ^ 2 ≤ 1) (hspec : (base hd rot hrot).SpectralBound lam) : (mergedN hn hd hm hN rot hrot).SpectralBound √(lam ^ 2 + (1 - lam ^ 2) / (2 * ↑m) + 1 / ↑m)

The spectral bound of the wide merge. The width enters only through the 1 / m terms, so the bound stays below one however far apart the sizes are.

Choosing the width

def Complexity.RegGraph.mergeWidth (N n : ℕ) : ℕ

A width that always works for folding N ≥ 2 n vertices onto n.

Equations

• Complexity.RegGraph.mergeWidth N n = N / n + 1

theorem Complexity.RegGraph.le_mergeWidth_mul (N : ℕ) {n : ℕ} (hn : 0 < n) : N ≤ mergeWidth N n * n

theorem Complexity.RegGraph.mergeWidth_sub_one_mul_le (N n : ℕ) : (mergeWidth N n - 1) * n ≤ N

theorem Complexity.RegGraph.three_le_mergeWidth {N n : ℕ} (hn : 0 < n) (h2 : 2 * n ≤ N) : 3 ≤ mergeWidth N n

theorem Complexity.RegGraph.mergeWidth_le {N n C : ℕ} (hn : 0 < n) (h : N ≤ C * n) : mergeWidth N n ≤ C + 1

The width is bounded whenever the overshoot is.