The hitting property of expander walks

A random walk on a good expander is unlikely to stay inside a small set of vertices for long. The study of this hitting property began with Ajtai, Komlós and Szemerédi; the sharp bound is due to Kahale, as credited in Vadhan, Section 4.6. We follow the operator-decomposition proof of Vadhan (Theorem 4.17), allowing a different set at each step and retaining the initial density factor. If the sets B 0, B 1, … all have density at most μ and λ = λ(G), a walk of length t from a uniformly random vertex has vᵢ ∈ B i for all i ≤ t with probability at most μ (μ + λ (1 - μ)) ^ t (Cslib.RotationMap.dens_filter_forall_walkAt_mem_le). The t + 1 vertices of the walk are sampled from a seed space of cardinality |V| * |D| ^ t, against |V| ^ (t + 1) for independent vertices. When μ < 1 and λ < 1, the probability of remaining in the sets decays exponentially in t. This is the probabilistic estimate underlying expander-walk error reduction for one-sided error; no machine-level error-reduction theorem is asserted here.

The expected product of weights h i at the vertices of a walk from v is computed by alternating the walk operator with multiplication by the weights (Cslib.RotationMap.weightedWalk, Cslib.RotationMap.expect_prod_walkAt). For indicator weights, each step multiplies the second moment of a function supported on a set of density at most μ by at most ((1 - λ) μ + λ) ^ 2: the walk operator is (1 - λ) times the projection onto the constants plus an operator of norm at most λ, and the projection of a function supported on a small set is small (Cslib.RotationMap.expect_ite_mem_walk_sq_le).

Main definitions

• Cslib.RotationMap.weightedWalk: the expected product of weights along a random walk.

Main results

• Cslib.RotationMap.expect_prod_walkAt: the expected product of weights along a walk from a vertex is the weighted walk.
• Cslib.RotationMap.expect_ite_mem_walk_sq_le: one step of a walk restricted to a small set.
• Cslib.RotationMap.dens_filter_forall_walkAt_mem_le: the hitting property.
• Cslib.RotationMap.dens_filter_forall_walkAt_mem_le_pow: the usual power bound for remaining in sets of density at most μ.
• Cslib.RotationMap.dens_filter_forall_walkAt_notMem_le: a walk misses a set of density δ with probability at most (1 - δ) (1 - (1 - λ) δ) ^ t.

References

• M. Ajtai, J. Komlós, E. Szemerédi, Deterministic simulation in LOGSPACE
• N. Kahale, Eigenvalues and expansion of regular graphs
• S. P. Vadhan, Pseudorandomness
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications

noncomputable def Cslib.RotationMap.weightedWalk {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] : ℕ → (ℕ → V → ℝ) → V → ℝ

The weighted walk G.weightedWalk t h: the function whose value at v is the expected product ∏_{i ≤ t} h i vᵢ of the weights h i at the vertices v₀ = v, v₁, …, v_t of a uniformly random walk of length t from v (expect_prod_walkAt). It multiplies by h 0 after a step of the walk operator applied to the weighted walk of the shifted weights.

@[simp]

theorem Cslib.RotationMap.weightedWalk_zero {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] (h : ℕ → V → ℝ) : G.weightedWalk 0 h = h 0

The weighted walk of length 0 is the weight h 0.

theorem Cslib.RotationMap.weightedWalk_succ {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] (t : ℕ) (h : ℕ → V → ℝ) : G.weightedWalk (t + 1) h = h 0 * G.walk (G.weightedWalk t fun (i : ℕ) => h (i + 1))

The weighted walk of length t + 1 multiplies by h 0 after a step of the walk operator applied to the weighted walk of length t of the shifted weights.

theorem Cslib.RotationMap.expect_prod_walkAt {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] (t : ℕ) (h : ℕ → V → ℝ) (v : V) : (Finset.univ.expect fun (k : Fin t → D) => ∏ i ∈ Finset.range (t + 1), h i (G.walkAt (v, k) i)) = G.weightedWalk t h v

The expected product of the weights h i at the vertices of a uniformly random walk of length t from v is the weighted walk at v.

theorem Cslib.RotationMap.expect_weightedWalk {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype D] [Fintype V] (t : ℕ) (h : ℕ → V → ℝ) : (Finset.univ.expect fun (v : V) => G.weightedWalk t h v) = Finset.univ.expect fun (p : V × (Fin t → D)) => ∏ i ∈ Finset.range (t + 1), h i (G.walkAt p i)

The average of the weighted walk is the expected product of the weights along a uniformly random walk.

theorem Cslib.RotationMap.expect_ite_mem_walk_sq_le {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] [DecidableEq V] [Nonempty D] {B C : Finset V} {μ : ℝ} (hB : ↑B.dens ≤ μ) (hC : ↑C.dens ≤ μ) {x : V → ℝ} (hx : ∀ v ∉ C, x v = 0) : (Finset.univ.expect fun (v : V) => (if v ∈ B then G.walk x v else 0) ^ 2) ≤ ((1 - G.spectralExpansion) * μ + G.spectralExpansion) ^ 2 * Finset.univ.expect fun (v : V) => x v ^ 2

One step of a walk restricted to a small set: if x vanishes outside a set C, and B and C have density at most μ, then restricting G.walk x to B gives second moment at most ((1 - λ(G)) μ + λ(G)) ^ 2 times that of x.

theorem Cslib.RotationMap.dens_filter_forall_walkAt_mem_le {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] [DecidableEq V] [Nonempty D] {B : ℕ → Finset V} {μ : ℝ} (hB : ∀ (i : ℕ), ↑(B i).dens ≤ μ) (t : ℕ) : ↑{p : V × (Fin t → D) | ∀ i ≤ t, G.walkAt p i ∈ B i}.dens ≤ μ * (μ + G.spectralExpansion * (1 - μ)) ^ t

The hitting property of expander walks, following Vadhan, Theorem 4.17 (the sharp bound is due to Kahale), with varying sets and the initial density factor retained: if the sets B i have density at most μ, a uniformly random walk of length t has its i-th vertex in B i for every i ≤ t with probability at most μ (μ + λ(G) (1 - μ)) ^ t.

theorem Cslib.RotationMap.dens_filter_forall_walkAt_mem_le_pow {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] [DecidableEq V] [Nonempty D] {B : ℕ → Finset V} {μ : ℝ} (hB : ∀ (i : ℕ), ↑(B i).dens ≤ μ) (hμ : μ ≤ 1) (t : ℕ) : ↑{p : V × (Fin t → D) | ∀ i ≤ t, G.walkAt p i ∈ B i}.dens ≤ (μ + G.spectralExpansion * (1 - μ)) ^ (t + 1)

The usual power form of the hitting bound: the probability that every vertex belongs to its specified set is at most (μ + λ(G) (1 - μ)) ^ (t + 1).

theorem Cslib.RotationMap.dens_filter_forall_walkAt_notMem_le {V : Type u_1} {D : Type u_2} (G : RotationMap V D) [Fintype V] [Fintype D] [DecidableEq V] [Nonempty V] [Nonempty D] (A : Finset V) (t : ℕ) : ↑{p : V × (Fin t → D) | ∀ i ≤ t, G.walkAt p i ∉ A}.dens ≤ (1 - ↑A.dens) * (1 - (1 - G.spectralExpansion) * ↑A.dens) ^ t

A uniformly started walk misses a set of density δ with probability at most (1 - δ) (1 - (1 - λ(G)) δ) ^ t.