The expander mixing lemma for t-step walks

The quantitative heart of every expander argument, in the square-norm form set up in RegularGraph: on a graph with SpectralBound lam, the correlation between a function f at the start of a t-step walk and a function g at its end is what independence would predict, up to lam ^ t times the two standard deviations.

Stated with everything squared, so no Real.sqrt appears:

(⟪f, Aᵗ g⟫ - (∑ f)(∑ g)/n) ^ 2 ≤ lam ^ (2t) · Var f · Var g

where Var f = ∑ f² - (∑ f)²/n is the (unnormalised) variance. Specialised to indicator functions of vertex sets this is the usual expander mixing lemma, and it is the estimate Dinur's powering step applies to the sets of vertices whose walk-labels disagree with a global assignment.

Main definitions

• RegGraph.mean, RegGraph.center — the mean of a function and its mean-zero part

Main results

• RegGraph.step_const, RegGraph.step_add, RegGraph.stepIter_const, RegGraph.stepIter_add — the walk operator is affine-linear and fixes constants
• RegGraph.sum_center, RegGraph.sum_sq_center — the Pythagoras identity splitting a function into its mean and its mean-zero part
• RegGraph.inner_stepIter_eq — the correlation splits into the independent part and a mean-zero correlation
• RegGraph.mixing_sq — the mixing lemma

Linearity of the walk operator

@[simp]

theorem Complexity.RegGraph.step_const (G : RegGraph) (c : ℝ) (v : G.V) : G.step (fun (x : G.V) => c) v = c

theorem Complexity.RegGraph.step_add (G : RegGraph) (f g : G.V → ℝ) (v : G.V) : G.step (fun (w : G.V) => f w + g w) v = G.step f v + G.step g v

theorem Complexity.RegGraph.stepIter_const (G : RegGraph) (t : ℕ) (c : ℝ) : (G.stepIter t fun (x : G.V) => c) = fun (x : G.V) => c

theorem Complexity.RegGraph.stepIter_add (G : RegGraph) (t : ℕ) (f g : G.V → ℝ) : (G.stepIter t fun (w : G.V) => f w + g w) = fun (v : G.V) => G.stepIter t f v + G.stepIter t g v

Centering

noncomputable def Complexity.RegGraph.mean (G : RegGraph) (f : G.V → ℝ) : ℝ

The mean of a function on the vertices.

Equations

• G.mean f = (∑ v : G.V, f v) / ↑G.order

noncomputable def Complexity.RegGraph.center (G : RegGraph) (f : G.V → ℝ) : G.V → ℝ

The mean-zero part of a function.

Equations

• G.center f v = f v - G.mean f

theorem Complexity.RegGraph.eq_mean_add_center (G : RegGraph) (f : G.V → ℝ) : f = fun (v : G.V) => G.mean f + G.center f v

theorem Complexity.RegGraph.sum_center (G : RegGraph) (hn : 0 < G.order) (f : G.V → ℝ) : ∑ v : G.V, G.center f v = 0

theorem Complexity.RegGraph.sum_sq_center (G : RegGraph) (hn : 0 < G.order) (f : G.V → ℝ) : ∑ v : G.V, G.center f v ^ 2 = ∑ v : G.V, f v ^ 2 - (∑ v : G.V, f v) ^ 2 / ↑G.order

theorem Complexity.RegGraph.sum_sq_center_nonneg (G : RegGraph) (f : G.V → ℝ) : 0 ≤ ∑ v : G.V, G.center f v ^ 2

The mixing lemma

theorem Complexity.RegGraph.inner_stepIter_eq (G : RegGraph) (hn : 0 < G.order) (t : ℕ) (f g : G.V → ℝ) : ∑ v : G.V, f v * G.stepIter t g v = ((∑ v : G.V, f v) * ∑ v : G.V, g v) / ↑G.order + ∑ v : G.V, G.center f v * G.stepIter t (G.center g) v

The correlation between f at the start of a t-step walk and g at its end splits into the product of averages plus the correlation of the mean-zero parts.

theorem Complexity.RegGraph.mixing_sq (G : RegGraph) {lam : ℝ} (h : G.SpectralBound lam) (hn : 0 < G.order) (t : ℕ) (f g : G.V → ℝ) : (∑ v : G.V, f v * G.stepIter t g v - ((∑ v : G.V, f v) * ∑ v : G.V, g v) / ↑G.order) ^ 2 ≤ lam ^ (2 * t) * (∑ v : G.V, f v ^ 2 - (∑ v : G.V, f v) ^ 2 / ↑G.order) * (∑ v : G.V, g v ^ 2 - (∑ v : G.V, g v) ^ 2 / ↑G.order)

The expander mixing lemma for t-step walks.