Each step of a random walk is a uniform dart

The counting fact behind every first-moment estimate in Dinur's powering analysis: fix a step index k < t; then the map sending a walk (v, s) to its k-th dart (walkAt k, s k) sends the uniform distribution on walks to the uniform distribution on darts. Equivalently, summing any function of the k-th dart over all order · deg ^ t walks gives deg ^ (t-1) times its sum over all darts — every dart is the k-th dart of exactly deg ^ (t-1) walks.

The proof is an induction on k that peels the first label off the walk. Two ingredients do the work: walkAt_cons, which says dropping the first label shifts the trajectory by one, and sum_nbr_nsmul, the rotation-map form of regularity, which reindexes the sum over (v, i) as deg copies of the sum over vertices.

Stated for an arbitrary AddCommMonoid, since it is used both to count walks in ℕ and to compute real-valued averages.

Main results

• RegGraph.walkAt_cons — dropping the first label shifts the trajectory
• RegGraph.sum_stepDart — the k-th dart of a uniform walk is a uniform dart
• RegGraph.sum_stepDart_fixed — from a fixed start, the k-th dart is described by the k-step walk operator
• RegGraph.card_walks_stepDart_mem — how many walks have their k-th dart in a given set

theorem Complexity.RegGraph.walkAt_cons (G : RegGraph) {t : ℕ} (v : G.V) (i : G.D) (s : Fin t → G.D) (m : ℕ) : G.walkAt (t + 1) v (Fin.cons i s) (m + 1) = G.walkAt t (G.nbr v i) s m

Dropping the first label of a walk shifts its trajectory by one step.

theorem Complexity.RegGraph.sum_stepDart (G : RegGraph) {M : Type u_1} [AddCommMonoid M] (k t : ℕ) (hk : k < t) (f : G.V × G.D → M) : ∑ v : G.V, ∑ s : Fin t → G.D, f (G.walkAt t v s k, s ⟨k, hk⟩) = G.deg ^ (t - 1) • ∑ p : G.V × G.D, f p

The k-th dart of a uniform walk is a uniform dart.

theorem Complexity.RegGraph.sum_cons_split (G : RegGraph) {M : Type u_1} [AddCommMonoid M] (m : ℕ) (F : (Fin (m + 1) → G.D) → M) : ∑ r : Fin (m + 1) → G.D, F r = ∑ i : G.D, ∑ r : Fin m → G.D, F (Fin.cons i r)

Summing over label tuples splits into the first label and the rest.

theorem Complexity.RegGraph.sum_stepDart_fixed (G : RegGraph) (h : G.V → G.D → ℝ) (k m : ℕ) (hk : k < m) (x : G.V) : ∑ r : Fin m → G.D, h (G.walkAt m x r k) (r ⟨k, hk⟩) = ↑G.deg ^ (m - 1) * ∑ a : G.D, G.stepIter k (fun (y : G.V) => h y a) x

The k-th dart of a walk out of a fixed start. Unlike sum_stepDart, where the start is also averaged and the dart comes out uniform, here the dart's vertex is distributed as the k-step walk from x, which the walk operator describes exactly. This is what turns a correlation between two steps of a walk into an operator inner product, where Mixing can bound it.

theorem Complexity.RegGraph.sum_two_darts_fixed (G : RegGraph) (h₁ h₂ : G.V → G.D → ℝ) (k l m : ℕ) (hkl : k < l) (hl : l < m) (x : G.V) : ∑ r : Fin m → G.D, h₁ (G.walkAt m x r k) (r ⟨k, ⋯⟩) * h₂ (G.walkAt m x r l) (r ⟨l, hl⟩) = ↑G.deg ^ (m - 2) * ∑ a : G.D, ∑ b : G.D, G.stepIter k (fun (y : G.V) => h₁ y a * G.stepIter (l - k - 1) (fun (z : G.V) => h₂ z b) (G.nbr y a)) x

Two darts of a walk out of a fixed start. The correlation between what happens at step k and at step l > k is an operator expression: the walk reaches step k, the constraint there is weighted, and the remaining l-k-1 steps are another application of the walk operator. Feeding this to Mixing is how the second moment of the number of faulty steps gets bounded.

theorem Complexity.RegGraph.card_walks_stepDart_mem (G : RegGraph) {t k : ℕ} (hk : k < t) (S : Finset (G.V × G.D)) : ∑ v : G.V, {s : Fin t → G.D | (G.walkAt t v s k, s ⟨k, hk⟩) ∈ S}.card = G.deg ^ (t - 1) * S.card

The number of walks of length t whose k-th dart lies in S.