Trajectories of walks, and self-loops

Walk gives the endpoint of a walk, which is all the spectral estimates need. Dinur's powering step also needs the walk's whole trajectory: the constraint attached to a length-t walk talks about the graph constraints on each intermediate edge, and about what the two endpoints of the walk claim the intermediate vertices are labelled.

This module adds the trajectory walkAt, indexed by ℕ and constant once the walk is exhausted, and identifies its final position with walkEnd. The bridge runs through walkEnd_snoc: extending a walk by one label at the end takes one more step from its endpoint, whereas walkEnd recurses on the first label.

It also introduces Loops, a choice of self-loop at each vertex. Dinur's construction needs these to pad a short walk out to a fixed length without moving: a vertex within distance k ≤ h of v is the endpoint of a length-h walk from v that follows k real steps and then stays put.

Main definitions

• RegGraph.walkAt — the position of the walk after k steps (k > t stays)
• RegGraph.Loops — a self-loop at every vertex
• RegGraph.Loops.padWalk — a short walk padded out to a fixed length

Main results

• RegGraph.walkEnd_snoc — appending a label takes one further step
• RegGraph.walkAt_eq_walkEnd_prefix, RegGraph.walkAt_self_eq_walkEnd
• RegGraph.walkAt_of_le — the trajectory is constant past its length
• RegGraph.Loops.nbr_loop — a loop label does not move
• RegGraph.Loops.walkEnd_padWalk — a padded walk of length h ends at the k-th vertex of the walk it pads, so every vertex within distance h is named by some length-h walk

Extending a walk at its end

theorem Complexity.RegGraph.walkEnd_snoc (G : RegGraph) (t : ℕ) (v : G.V) (s : Fin t → G.D) (i : G.D) : G.walkEnd (t + 1) v (Fin.snoc s i) = G.nbr (G.walkEnd t v s) i

The trajectory

def Complexity.RegGraph.walkAt (G : RegGraph) (t : ℕ) (v : G.V) (s : Fin t → G.D) : ℕ → G.V

The position of the walk (v, s) after k steps. Once the label tuple is exhausted the walk stays where it is, so this is defined for every k : ℕ.

Equations

• G.walkAt t v s 0 = v
• G.walkAt t v s k.succ = if h : k < t then G.nbr (G.walkAt t v s k) (s ⟨k, h⟩) else G.walkAt t v s k

@[simp]

theorem Complexity.RegGraph.walkAt_zero (G : RegGraph) (t : ℕ) (v : G.V) (s : Fin t → G.D) : G.walkAt t v s 0 = v

theorem Complexity.RegGraph.walkAt_succ_of_lt (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) {k : ℕ} (h : k < t) : G.walkAt t v s (k + 1) = G.nbr (G.walkAt t v s k) (s ⟨k, h⟩)

theorem Complexity.RegGraph.walkAt_succ_of_ge (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) {k : ℕ} (h : t ≤ k) : G.walkAt t v s (k + 1) = G.walkAt t v s k

theorem Complexity.RegGraph.walkAt_of_le (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) {k : ℕ} : t ≤ k → G.walkAt t v s k = G.walkAt t v s t

Past its length the trajectory is constant.

theorem Complexity.RegGraph.walkAt_eq_walkEnd_prefix (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) (k : ℕ) (hk : k ≤ t) : G.walkAt t v s k = G.walkEnd k v fun (j : Fin k) => s (Fin.castLE hk j)

The trajectory after k ≤ t steps is the endpoint of the length-k prefix of the walk.

theorem Complexity.RegGraph.walkAt_self_eq_walkEnd (G : RegGraph) {t : ℕ} (v : G.V) (s : Fin t → G.D) : G.walkAt t v s t = G.walkEnd t v s

The trajectory ends where walkEnd says it does.

Self-loops

structure Complexity.RegGraph.Loops (G : RegGraph) : Type

A choice of self-loop at every vertex: an edge label that fixes the dart, hence does not move. Dinur's construction needs these to pad short walks out to a fixed length.

• loop : G.V → G.D

  The self-loop label at each vertex.

• rot_loop (v : G.V) : G.rot (v, self.loop v) = (v, self.loop v)

  The chosen dart is fixed by reversal, so it is a self-loop.

@[simp]

theorem Complexity.RegGraph.Loops.nbr_loop {G : RegGraph} (L : G.Loops) (v : G.V) : G.nbr v (L.loop v) = v

Following a loop label does not move.

def Complexity.RegGraph.Loops.padWalk {G : RegGraph} (L : G.Loops) {t : ℕ} (v : G.V) (s : Fin t → G.D) (k h : ℕ) : Fin h → G.D

The length-h label tuple that follows s for k steps and then stays put, taking self-loops. This is how a vertex within distance k ≤ h of v is named by a walk of length exactly h out of v.

Equations

• L.padWalk v s k h j = if hj : ↑j < min k t then s ⟨↑j, ⋯⟩ else L.loop (G.walkAt t v s k)

theorem Complexity.RegGraph.Loops.padWalk_of_lt {G : RegGraph} (L : G.Loops) {t : ℕ} (v : G.V) (s : Fin t → G.D) {k h : ℕ} (j : Fin h) (hj : ↑j < min k t) : L.padWalk v s k h j = s ⟨↑j, ⋯⟩

theorem Complexity.RegGraph.Loops.padWalk_of_ge {G : RegGraph} (L : G.Loops) {t : ℕ} (v : G.V) (s : Fin t → G.D) {k h : ℕ} (j : Fin h) (hj : ¬↑j < min k t) : L.padWalk v s k h j = L.loop (G.walkAt t v s k)

theorem Complexity.RegGraph.Loops.walkAt_padWalk_of_le {G : RegGraph} (L : G.Loops) {t : ℕ} (v : G.V) (s : Fin t → G.D) {k h : ℕ} (hkh : k ≤ h) (hkt : k ≤ t) (m : ℕ) : m ≤ k → G.walkAt h v (L.padWalk v s k h) m = G.walkAt t v s m

Below k the padded walk follows the original.

theorem Complexity.RegGraph.Loops.walkAt_padWalk_of_ge {G : RegGraph} (L : G.Loops) {t : ℕ} (v : G.V) (s : Fin t → G.D) {k h : ℕ} (hkh : k ≤ h) (hkt : k ≤ t) (m : ℕ) : k ≤ m → m ≤ h → G.walkAt h v (L.padWalk v s k h) m = G.walkAt t v s k

At and past k the padded walk stays at the k-th vertex.

theorem Complexity.RegGraph.Loops.walkEnd_padWalk {G : RegGraph} (L : G.Loops) {t : ℕ} (v : G.V) (s : Fin t → G.D) {k h : ℕ} (hkh : k ≤ h) (hkt : k ≤ t) : G.walkEnd h v (L.padWalk v s k h) = G.walkAt t v s k

The naming property. A padded walk of length h ends exactly at the k-th vertex of the original walk.