Walks on rotation maps

A walk of length t in a D-regular multigraph G on V is a start vertex together with t labels, p : V × (Fin t → D), and takes the edges labelled p.2 0, …, p.2 (t - 1) in turn. There are |V| |D| ^ t of them, and they are the darts of the power G.pow t. Walks are the combinatorial side of the powering step of Dinur's proof of the PCP theorem Dinur, Sections 3.2 and 5 Arora and Barak, Chapter 22, whose analysis counts the steps of a random walk that cross a given set of edges; this file provides the facts about walks that analysis rests on.

The trajectory G.walkAt p i is the vertex reached after i steps (constant after the last step) and G.walkDart p i is the edge taken at step i, as a dart. A walk ends at (G.pow t).neighbor p.1 p.2 (walkAt_length), so averaging over the labels from a fixed start is applying the walk operator G.walk ^ t (expect_walkAt_length, through walk_pow), and the rotation map of G.pow t reverses walks: it reverses the trajectory (walkAt_rot_pow) and the darts, each seen from its other end (walkDart_rot_pow), and it reverses the steps after the n-th into the first t - n steps of the reverse (rot_pow_walkDrop).

Splitting a walk at its i-th step into the dart q taken there, the reverse of the first i steps, which leads back from q to the start, and the steps after it, which lead on from the far end of q, is a bijection splitWalk i onto (V × D) × (Fin i → D) × (Fin (t - (i + 1)) → D). So the three pieces of a uniformly random walk are independent and uniform (expect_splitWalk), and walks crossing a dart with conditions on the two pieces are counted by independent factors (card_filter_splitWalk). In particular each step of a random walk is a uniformly random dart (expect_walkDart): every dart is the i-th dart of |D| ^ (t - 1) walks of length t (sum_walkDart, card_filter_walkDart_eq). This is the fact behind the first-moment estimate of the powering step.

For steps i < j, the correlation of a function of the i-th dart with a function of the j-th dart is a correlation along j - (i + 1) steps of the random walk (expect_walkDart_mul_walkDart), so the mixing lemma bounds its distance to the product of the averages by λ(G) ^ (j - (i + 1)) times the standard deviations (sq_expect_walkDart_mul_walkDart_sub_le). Summed over the pairs of steps, this is the second-moment estimate of the powering step.

Main definitions

• Cslib.RotationMap.walkAt: the vertex of a walk after i steps.
• Cslib.RotationMap.walkDart: the dart of a walk at step i.
• Cslib.RotationMap.walkDrop: the walk after the first n steps of a walk.
• Cslib.RotationMap.splitWalk: splitting a walk at a step into the dart taken there, the reverse of the steps before it and the steps after it.

Main results

• Cslib.RotationMap.walkAt_length, Cslib.RotationMap.expect_walkAt_length: a walk ends at its neighbor in G.pow t, so averaging over the walks from a vertex applies G.walk ^ t.
• Cslib.RotationMap.walkAt_rot_pow, Cslib.RotationMap.walkDart_rot_pow, Cslib.RotationMap.rot_pow_walkDrop: the rotation map of G.pow t reverses walks.
• Cslib.RotationMap.expect_splitWalk, Cslib.RotationMap.card_filter_splitWalk: the pieces of a walk split at a step are independent and uniform.
• Cslib.RotationMap.expect_walkDart, Cslib.RotationMap.sum_walkDart: each step of a random walk is a uniformly random dart.
• Cslib.RotationMap.expect_walkDart_mul_walkDart: the correlation of two darts of a random walk is a correlation along the walk operator.
• Cslib.RotationMap.sq_expect_walkDart_mul_walkDart_sub_le, Cslib.RotationMap.abs_expect_walkDart_mul_walkDart_sub_le: two darts of a random walk are almost independent.

References

• I. Dinur, The PCP theorem by gap amplification
• I. Dinur, The PCP theorem by gap amplification, ECCC TR05-046, revision 1
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

def Cslib.RotationMap.walkAt {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) : ℕ → V

The vertex reached after i steps of the walk p = (v, k) of length t, which starts at v and takes the edges labelled k 0, …, k (t - 1) in turn. After its last step the walk stays at its end: G.walkAt p i = G.walkAt p t for t ≤ i (walkAt_of_le).

@[simp]

theorem Cslib.RotationMap.walkAt_zero {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) : G.walkAt p 0 = p.1

A walk starts at its first vertex.

theorem Cslib.RotationMap.walkAt_succ_of_lt {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) {i : ℕ} (h : i < t) : G.walkAt p (i + 1) = G.neighbor (G.walkAt p i) (p.2 ⟨i, h⟩)

At its step i + 1 ≤ t, a walk moves along its i-th label.

theorem Cslib.RotationMap.walkAt_succ_of_le {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) {i : ℕ} (h : t ≤ i) : G.walkAt p (i + 1) = G.walkAt p i

After its last step, a walk does not move.

theorem Cslib.RotationMap.walkAt_of_le {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) {i : ℕ} (h : t ≤ i) : G.walkAt p i = G.walkAt p t

After its last step a walk stays at its end.

def Cslib.RotationMap.walkDart {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (i : Fin t) : V × D

The i-th dart of the walk p: the edge taken at step i, seen from the vertex where it is taken.

@[simp]

theorem Cslib.RotationMap.walkDart_fst {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (i : Fin t) : (G.walkDart p i).1 = G.walkAt p ↑i

The i-th dart of a walk starts at its i-th vertex.

@[simp]

theorem Cslib.RotationMap.walkDart_snd {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (i : Fin t) : (G.walkDart p i).2 = p.2 i

The i-th dart of a walk has its i-th label.

theorem Cslib.RotationMap.fst_rot_walkDart {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (i : Fin t) : (G.rot (G.walkDart p i)).1 = G.walkAt p (↑i + 1)

The i-th dart of a walk leads to its (i + 1)-th vertex.

theorem Cslib.RotationMap.walkAt_cons_succ {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (v : V) (a : D) (k : Fin t → D) (i : ℕ) : G.walkAt (v, Fin.cons a k) (i + 1) = G.walkAt (G.neighbor v a, k) i

A walk whose first label is a takes the edge a and then walks along the remaining labels.

theorem Cslib.RotationMap.walkDart_cons_succ {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (v : V) (a : D) (k : Fin t → D) (i : Fin t) : G.walkDart (v, Fin.cons a k) i.succ = G.walkDart (G.neighbor v a, k) i

The (i + 1)-th dart of a walk whose first label is a is the i-th dart of the walk along the remaining labels from the neighbor along a.

theorem Cslib.RotationMap.walkAt_take {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) {n i : ℕ} (hn : n ≤ t) (hi : i ≤ n) : G.walkAt (p.1, Fin.take n hn p.2) i = G.walkAt p i

The walk along the first n labels of a walk follows it for n steps.

theorem Cslib.RotationMap.walkDart_take {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) {n : ℕ} (hn : n ≤ t) (i : Fin n) : G.walkDart (p.1, Fin.take n hn p.2) i = G.walkDart p (Fin.castLE hn i)

The darts of the walk along the first n labels of a walk are its first n darts.

theorem Cslib.RotationMap.walkAt_snoc {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (v : V) (k : Fin t → D) (a : D) {i : ℕ} (hi : i ≤ t) : G.walkAt (v, Fin.snoc k a) i = G.walkAt (v, k) i

Appending a label to a walk does not change its first t steps.

theorem Cslib.RotationMap.walkDart_snoc_castSucc {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (v : V) (k : Fin t → D) (a : D) (i : Fin t) : G.walkDart (v, Fin.snoc k a) i.castSucc = G.walkDart (v, k) i

The i-th dart of a walk extended by a label a is the i-th dart of the walk.

def Cslib.RotationMap.walkDrop {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (n : ℕ) : V × (Fin (t - n) → D)

The walk along the labels of p after its n-th step, from the n-th vertex of p.

@[simp]

theorem Cslib.RotationMap.walkDrop_fst {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (n : ℕ) : (G.walkDrop p n).1 = G.walkAt p n

The walk after the n-th step of p starts at the n-th vertex of p.

theorem Cslib.RotationMap.walkDrop_snd_apply {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (n : ℕ) (j : Fin (t - n)) : (G.walkDrop p n).2 j = p.2 ⟨n + ↑j, ⋯⟩

The labels of the walk after the n-th step of p are the remaining labels of p.

theorem Cslib.RotationMap.walkAt_walkDrop {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (n i : ℕ) : G.walkAt (G.walkDrop p n) i = G.walkAt p (n + i)

The walk after the n-th step of p follows p from its n-th vertex on.

theorem Cslib.RotationMap.walkDart_walkDrop {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (n : ℕ) (j : Fin (t - n)) : G.walkDart (G.walkDrop p n) j = G.walkDart p ⟨n + ↑j, ⋯⟩

The j-th dart of the walk after the n-th step of p is the (n + j)-th dart of p.

theorem Cslib.RotationMap.walkAt_length {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) : G.walkAt p t = (G.pow t).neighbor p.1 p.2

A walk of length t ends at the neighbor along its labels in the power G ^ t.

theorem Cslib.RotationMap.walkAt_eq_neighbor_pow {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) {n : ℕ} (hn : n ≤ t) : G.walkAt p n = (G.pow n).neighbor p.1 (Fin.take n hn p.2)

The n-th vertex of a walk is the neighbor along its first n labels in the power G ^ n.

theorem Cslib.RotationMap.walkDart_rot_pow {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (i : Fin t) : G.walkDart ((G.pow t).rot p) i = G.rot (G.walkDart p i.rev)

Reversing a walk in G ^ t reverses its darts: the i-th dart of the reverse of p is the (t - 1 - i)-th dart of p seen from its other end.

theorem Cslib.RotationMap.walkAt_rot_pow {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) {i : ℕ} (hi : i ≤ t) : G.walkAt ((G.pow t).rot p) i = G.walkAt p (t - i)

Reversing a walk in G ^ t reverses its trajectory.

theorem Cslib.RotationMap.rot_pow_walkDrop {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) (n : ℕ) : (G.pow (t - n)).rot (G.walkDrop p n) = (((G.pow t).rot p).1, Fin.take (t - n) ⋯ ((G.pow t).rot p).2)

The reverse of the walk after the n-th step of p is the walk along the first t - n labels of the reverse of p.

theorem Cslib.RotationMap.expect_walkAt_length {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype D] (v : V) (f : V → ℝ) : (Finset.univ.expect fun (k : Fin t → D) => f (G.walkAt (v, k) t)) = (G.walk ^ t) f v

Averaged over its labels, a walk of length t from v ends where the random walk is after t steps: the average of f over its ends is (G.walk ^ t) f v.

theorem Cslib.RotationMap.expect_mul_walkAt_length {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype D] [Fintype V] (f g : V → ℝ) : (Finset.univ.expect fun (p : V × (Fin t → D)) => f p.1 * g (G.walkAt p t)) = Finset.univ.expect fun (v : V) => f v * (G.walk ^ t) g v

The correlation of f at the start with g at the end of a uniformly random walk of length t is 𝔼 v, f v * (G.walk ^ t) g v, the quantity estimated by the mixing lemma sq_expect_mul_walk_pow_sub_le.

def Cslib.RotationMap.splitWalk {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (i : Fin t) : V × (Fin t → D) ≃ (V × D) × (Fin ↑i → D) × (Fin (t - (↑i + 1)) → D)

Splitting a walk at its i-th step. A walk p of length t is determined by its i-th dart q, the labels r of the reverse of its first i steps, which lead back from the start of q to the start of p, and its labels s after step i, which lead on from the end of q; and any such data come from a walk. So (q, r, s) ranges over all of (V × D) × (Fin i → D) × (Fin (t - (i + 1)) → D) as p ranges over the walks: q is the crossed dart, (q.1, r) the walk back to the start (fst_rot_pow_take, walkAt_rot_pow_take) and ((G.rot q).1, s) the walk on to the end (fst_rot_walkDart, walkAt_walkDrop). The inverse glues a walk from these pieces.

theorem Cslib.RotationMap.splitWalk_apply {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (i : Fin t) (p : V × (Fin t → D)) : (G.splitWalk i) p = (G.walkDart p i, ((G.pow ↑i).rot (p.1, Fin.take ↑i ⋯ p.2)).2, (G.walkDrop p (↑i + 1)).2)

The pieces of a walk split at its i-th step.

theorem Cslib.RotationMap.fst_rot_pow_take {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) {n : ℕ} (hn : n ≤ t) : ((G.pow n).rot (p.1, Fin.take n hn p.2)).1 = G.walkAt p n

The reverse of the first n steps of a walk starts at its n-th vertex.

theorem Cslib.RotationMap.walkAt_rot_pow_take {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} (p : V × (Fin t → D)) {n i : ℕ} (hn : n ≤ t) (hi : i ≤ n) : G.walkAt ((G.pow n).rot (p.1, Fin.take n hn p.2)) i = G.walkAt p (n - i)

The reverse of the first n steps of a walk retraces them.

theorem Cslib.RotationMap.expect_splitWalk {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype V] [Fintype D] {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (i : Fin t) (F : (V × D) × (Fin ↑i → D) × (Fin (t - (↑i + 1)) → D) → M) : (Finset.univ.expect fun (p : V × (Fin t → D)) => F ((G.splitWalk i) p)) = Finset.univ.expect fun (q : V × D) => Finset.univ.expect fun (r : Fin ↑i → D) => Finset.univ.expect fun (s : Fin (t - (↑i + 1)) → D) => F (q, r, s)

The pieces of a uniformly random walk are independent and uniform. Split at its i-th step, a uniformly random walk of length t has a uniformly random i-th dart, and independently of it uniformly random labels before and after it.

theorem Cslib.RotationMap.card_filter_splitWalk {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype V] [Fintype D] (i : Fin t) (P : V × D → (Fin ↑i → D) → Prop) (Q : V × D → (Fin (t - (↑i + 1)) → D) → Prop) [(q : V × D) → DecidablePred (P q)] [(q : V × D) → DecidablePred (Q q)] : {p : V × (Fin t → D) | P (G.walkDart p i) ((G.pow ↑i).rot (p.1, Fin.take ↑i ⋯ p.2)).2 ∧ Q (G.walkDart p i) (G.walkDrop p (↑i + 1)).2}.card = ∑ q : V × D, {r : Fin ↑i → D | P q r}.card * {s : Fin (t - (↑i + 1)) → D | Q q s}.card

The crossing count. Counted by their i-th dart q, the walks of length t for which the reverse of the first i steps satisfies P q and the steps after the i-th satisfy Q q are counted by independent factors.

theorem Cslib.RotationMap.sum_walkDart {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype V] [Fintype D] {M : Type u_3} [AddCommMonoid M] (i : Fin t) (f : V × D → M) : ∑ p : V × (Fin t → D), f (G.walkDart p i) = Fintype.card D ^ (t - 1) • ∑ q : V × D, f q

Each step of a walk is a uniform dart (counting form): summing a function of the i-th dart over the walks of length t sums it |D| ^ (t - 1) times over the darts, for every dart is the i-th dart of |D| ^ (t - 1) walks.

theorem Cslib.RotationMap.expect_walkDart {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype V] [Fintype D] {M : Type u_3} [AddCommMonoid M] [Module ℚ≥0 M] (i : Fin t) (f : V × D → M) : (Finset.univ.expect fun (p : V × (Fin t → D)) => f (G.walkDart p i)) = Finset.univ.expect fun (q : V × D) => f q

Each step of a uniformly random walk is a uniformly random dart.

theorem Cslib.RotationMap.card_filter_walkDart_mem {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype V] [Fintype D] [DecidableEq V] [DecidableEq D] (i : Fin t) (S : Finset (V × D)) : {p : V × (Fin t → D) | G.walkDart p i ∈ S}.card = Fintype.card D ^ (t - 1) * S.card

The walks of length t whose i-th dart lies in S number |D| ^ (t - 1) * |S|.

theorem Cslib.RotationMap.card_filter_walkDart_eq {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype V] [Fintype D] [DecidableEq V] [DecidableEq D] (i : Fin t) (q : V × D) : {p : V × (Fin t → D) | G.walkDart p i = q}.card = Fintype.card D ^ (t - 1)

Every dart is the i-th dart of |D| ^ (t - 1) walks of length t.

theorem Cslib.RotationMap.expect_walkDart_mul_walkDart {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype D] [Fintype V] {i j : Fin t} (hij : i < j) (f g : V × D → ℝ) : (Finset.univ.expect fun (p : V × (Fin t → D)) => f (G.walkDart p i) * g (G.walkDart p j)) = Finset.univ.expect fun (v : V) => (Finset.univ.expect fun (a : D) => f (G.rot (v, a))) * (G.walk ^ (↑j - (↑i + 1))) (fun (w : V) => Finset.univ.expect fun (a : D) => g (w, a)) v

Two darts of a random walk. For steps i < j of a uniformly random walk, the correlation of f at the i-th dart with g at the j-th dart is the correlation, along j - (i + 1) steps of the random walk, of the average 𝔼 a, f (G.rot (v, a)) of f over the darts into a vertex v with the average 𝔼 a, g (w, a) of g over the darts out of a vertex w.

theorem Cslib.RotationMap.sq_expect_walkDart_mul_walkDart_sub_le {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype D] [Fintype V] {i j : Fin t} (hij : i < j) (f g : V × D → ℝ) : ((Finset.univ.expect fun (p : V × (Fin t → D)) => f (G.walkDart p i) * g (G.walkDart p j)) - (Finset.univ.expect fun (q : V × D) => f q) * Finset.univ.expect fun (q : V × D) => g q) ^ 2 ≤ G.spectralExpansion ^ (2 * (↑j - (↑i + 1))) * ((Finset.univ.expect fun (q : V × D) => f q ^ 2) - (Finset.univ.expect fun (q : V × D) => f q) ^ 2) * ((Finset.univ.expect fun (q : V × D) => g q ^ 2) - (Finset.univ.expect fun (q : V × D) => g q) ^ 2)

Two darts of a random walk are almost independent. For steps i < j of a uniformly random walk, the correlation of f at the i-th dart with g at the j-th dart differs from the product of their averages over the darts by at most λ(G) ^ (j - (i + 1)) times their standard deviations. Squared: the square of the difference is at most λ(G) ^ (2 (j - (i + 1))) times the product of the variances 𝔼 f² - (𝔼 f)² and 𝔼 g² - (𝔼 g)².

theorem Cslib.RotationMap.abs_expect_walkDart_mul_walkDart_sub_le {V : Type u_1} {D : Type u_2} (G : RotationMap V D) {t : ℕ} [Fintype D] [Fintype V] {i j : Fin t} (hij : i < j) (f : V × D → ℝ) : |(Finset.univ.expect fun (p : V × (Fin t → D)) => f (G.walkDart p i) * f (G.walkDart p j)) - (Finset.univ.expect fun (q : V × D) => f q) ^ 2| ≤ G.spectralExpansion ^ (↑j - (↑i + 1)) * ((Finset.univ.expect fun (q : V × D) => f q ^ 2) - (Finset.univ.expect fun (q : V × D) => f q) ^ 2)

Two darts of a random walk are almost independent: for steps i < j of a uniformly random walk, the correlation of f at the i-th dart with f at the j-th dart differs from the square of its average over the darts by at most λ(G) ^ (j - (i + 1)) times its variance.