Walks in a regular graph

Dinur's powering step replaces the edges of a constraint graph by its walks of a fixed length t. This module gives walks their combinatorial form — a starting vertex together with a tuple of t edge labels — and connects that form to the analytic one: summing any function of the walk's endpoint over all deg ^ t walks out of a vertex is deg ^ t times the t-step walk operator.

That identity, sum_walkEnd, is the bridge between the two views. The powering construction is defined by quantifying over walk tuples, while every estimate about it comes from the spectral bound through Mixing; sum_mul_walkEnd performs the translation in the form the analysis needs.

Main definitions

• RegGraph.walkEnd — the endpoint of the walk from v with label tuple s

Main results

• RegGraph.sum_walkEnd — ∑ s, f (walkEnd v s) = d ^ t * stepIter t f v
• RegGraph.sum_mul_walkEnd — the correlation of f at the start and g at the end of a random walk, as a multiple of the operator inner product
• RegGraph.card_walks — there are deg ^ t walks out of each vertex

def Complexity.RegGraph.walkEnd (G : RegGraph) (t : ℕ) : G.V → (Fin t → G.D) → G.V

The endpoint of the walk that starts at v and follows the edge labels s 0, s 1, …, s (t-1) in order.

Equations

• G.walkEnd 0 x✝ x_3 = x✝
• G.walkEnd t.succ x✝ s = G.walkEnd t (G.nbr x✝ (s 0)) fun (j : Fin t) => s j.succ

@[simp]

theorem Complexity.RegGraph.walkEnd_zero (G : RegGraph) (v : G.V) (s : Fin 0 → G.D) : G.walkEnd 0 v s = v

theorem Complexity.RegGraph.walkEnd_succ (G : RegGraph) (t : ℕ) (v : G.V) (s : Fin (t + 1) → G.D) : G.walkEnd (t + 1) v s = G.walkEnd t (G.nbr v (s 0)) fun (j : Fin t) => s j.succ

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

theorem Complexity.RegGraph.card_walks (G : RegGraph) (t : ℕ) : Fintype.card (Fin t → G.D) = G.deg ^ t

There are deg ^ t walks of length t out of a vertex.

theorem Complexity.RegGraph.sum_walkEnd (G : RegGraph) (f : G.V → ℝ) (t : ℕ) (v : G.V) : ∑ s : Fin t → G.D, f (G.walkEnd t v s) = ↑G.deg ^ t * G.stepIter t f v

The bridge between walks and the walk operator. Averaging a function of the endpoint over all walks of length t out of v is exactly the t-step operator applied at v.

theorem Complexity.RegGraph.sum_mul_walkEnd (G : RegGraph) (f g : G.V → ℝ) (t : ℕ) : ∑ v : G.V, ∑ s : Fin t → G.D, f v * g (G.walkEnd t v s) = ↑G.deg ^ t * ∑ v : G.V, f v * G.stepIter t g v

The walk-form of the correlation between the start and the end of a random walk: it is deg ^ t times the operator inner product, which mixing_sq estimates.