The expander mixing lemma

On a regular graph of small spectral expansion λ(G), edges are spread out as in a random graph: the number of edges between two sets of vertices is close to what a random graph of the same density would have.

For real functions on the vertices, with expectations taken over uniform vertices, the correlation of f at the start of a walk of length t with g at its end is the product of the expectations up to λ(G) ^ t times the two standard deviations (sq_expect_mul_walk_pow_sub_le). Applied to the indicator functions of two sets S and T of vertices, this is the expander mixing lemma Arora and Barak, Section 21.2 Hoory, Linial and Wigderson, Lemma 2.5, in the sharper form

|e(S, T) - d |S| |T| / n| ≤ λ(G) d √(|S| |Sᶜ| |T| |Tᶜ|) / n

(abs_card_interedges_sub_le), for a d-regular graph on n vertices, where e(S, T) counts the edges from S to T with those inside S ∩ T counted twice.

For T = Sᶜ a one-sided bound suffices: at least (1 - μ) d |S| |Sᶜ| / n edges leave S as soon as 𝔼 f · G.walk f ≤ μ 𝔼 f² for all f of expectation zero (le_card_interedges_compl_of_expect_mul_walk_le). This is the easy half of the discrete Cheeger inequality Hoory, Linial and Wigderson, Theorem 2.4; with μ = λ(G) it says that spectral expanders are edge expanders Arora and Barak, Section 21.2 (le_card_interedges_compl, le_card_interedges_compl_of_two_mul_card_le).

Main results

• Cslib.RotationMap.expect_mul_walk_pow_eq: the correlation along a walk is the product of the expectations plus the correlation of the centered functions.
• Cslib.RotationMap.sq_expect_mul_walk_pow_sub_le: the mixing lemma for functions and walks of any length.
• Cslib.RotationMap.abs_expect_mul_walk_le: |𝔼 f · G.walk f| ≤ λ(G) 𝔼 f² for f of expectation zero.
• Cslib.RotationMap.abs_card_interedges_sub_le, Cslib.RotationMap.abs_card_interedges_sub_le_mul_sqrt: the expander mixing lemma.
• Cslib.RotationMap.le_card_interedges_compl_of_expect_mul_walk_le, Cslib.RotationMap.le_card_interedges_compl: edge expansion from a spectral bound.
• Cslib.RotationMap.le_card_interedges_compl_of_two_mul_card_le: a set of at most half of the vertices has at least (1 - λ(G)) d |S| / 2 edges leaving it.
• Cslib.RotationMap.mul_card_filter_ne_le_card_filter_ne_neighbor: an expander has many edges between differently labelled vertices.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications

theorem Cslib.RotationMap.expect_mul_walk_pow_eq {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [Nonempty D] (t : ℕ) (f g : V → ℝ) : (Finset.univ.expect fun (v : V) => f v * (G.walk ^ t) g v) = ((Finset.univ.expect fun (v : V) => f v) * Finset.univ.expect fun (v : V) => g v) + Finset.univ.expect fun (v : V) => (f v - Finset.univ.expect fun (w : V) => f w) * (G.walk ^ t) (fun (w : V) => g w - Finset.univ.expect fun (u : V) => g u) v

The correlation of f with g along walks of length t is the product of the expectations plus the correlation of the centered functions.

theorem Cslib.RotationMap.sq_expect_mul_walk_pow_sub_le {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [Nonempty D] (t : ℕ) (f g : V → ℝ) : ((Finset.univ.expect fun (v : V) => f v * (G.walk ^ t) g v) - (Finset.univ.expect fun (v : V) => f v) * Finset.univ.expect fun (v : V) => g v) ^ 2 ≤ G.spectralExpansion ^ (2 * t) * ((Finset.univ.expect fun (v : V) => f v ^ 2) - (Finset.univ.expect fun (v : V) => f v) ^ 2) * ((Finset.univ.expect fun (v : V) => g v ^ 2) - (Finset.univ.expect fun (v : V) => g v) ^ 2)

The mixing lemma for functions: the correlation 𝔼 v, f v * (G.walk ^ t) g v of f with g along walks of length t differs from the product of their expectations by at most λ(G) ^ t times their standard deviations. Squared: the square of the difference is at most λ(G) ^ (2 t) times the product of the variances 𝔼 f² - (𝔼 f)² and 𝔼 g² - (𝔼 g)².

theorem Cslib.RotationMap.abs_expect_mul_walk_le {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) {f : V → ℝ} (hf : (Finset.univ.expect fun (v : V) => f v) = 0) : |Finset.univ.expect fun (v : V) => f v * G.walk f v| ≤ G.spectralExpansion * Finset.univ.expect fun (v : V) => f v ^ 2

For f of expectation zero, the correlation 𝔼 v, f v * G.walk f v is at most λ(G) times the second moment of f in absolute value.

theorem Cslib.RotationMap.abs_card_interedges_sub_le {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] (S T : Finset V) : |↑(G.interedges S T).card - ↑(Fintype.card D) * ↑S.card * ↑T.card / ↑(Fintype.card V)| ≤ G.spectralExpansion * ↑(Fintype.card D) * √(↑S.card * ↑Sᶜ.card * ↑T.card * ↑Tᶜ.card) / ↑(Fintype.card V)

The expander mixing lemma Arora and Barak, Section 21.2 Hoory, Linial and Wigderson, Lemma 2.5, sharper form: in a d-regular graph on n vertices, the number of edges from S to T differs from d |S| |T| / n by at most λ(G) d √(|S| |Sᶜ| |T| |Tᶜ|) / n.

theorem Cslib.RotationMap.abs_card_interedges_sub_le_mul_sqrt {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] (S T : Finset V) : |↑(G.interedges S T).card - ↑(Fintype.card D) * ↑S.card * ↑T.card / ↑(Fintype.card V)| ≤ G.spectralExpansion * ↑(Fintype.card D) * √(↑S.card * ↑T.card)

The expander mixing lemma in its usual form Arora and Barak, Section 21.2 Hoory, Linial and Wigderson, Lemma 2.5: in a d-regular graph on n vertices, the number of edges from S to T differs from d |S| |T| / n by at most λ(G) d √(|S| |T|).

theorem Cslib.RotationMap.le_card_interedges_compl_of_expect_mul_walk_le {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] {μ : ℝ} (hμ : ∀ (f : V → ℝ), (Finset.univ.expect fun (v : V) => f v) = 0 → (Finset.univ.expect fun (v : V) => f v * G.walk f v) ≤ μ * Finset.univ.expect fun (v : V) => f v ^ 2) (S : Finset V) : (1 - μ) * ↑(Fintype.card D) * ↑S.card * ↑Sᶜ.card / ↑(Fintype.card V) ≤ ↑(G.interedges S Sᶜ).card

Edge expansion from a one-sided spectral bound: if 𝔼 v, f v * G.walk f v ≤ μ 𝔼 f² for every function f of expectation zero, then in a d-regular graph on n vertices at least (1 - μ) d |S| |Sᶜ| / n edges leave S. The best such μ is the second largest eigenvalue of the walk operator, so this is the easy half of the discrete Cheeger inequality Hoory, Linial and Wigderson, Theorem 2.4.

theorem Cslib.RotationMap.le_card_interedges_compl {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] (S : Finset V) : (1 - G.spectralExpansion) * ↑(Fintype.card D) * ↑S.card * ↑Sᶜ.card / ↑(Fintype.card V) ≤ ↑(G.interedges S Sᶜ).card

Spectral expanders are edge expanders Arora and Barak, Section 21.2: in a d-regular graph on n vertices, at least (1 - λ(G)) d |S| |Sᶜ| / n edges leave S.

theorem Cslib.RotationMap.le_card_interedges_compl_of_two_mul_card_le {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] {S : Finset V} (hS : 2 * S.card ≤ Fintype.card V) : (1 - G.spectralExpansion) * ↑(Fintype.card D) * ↑S.card / 2 ≤ ↑(G.interedges S Sᶜ).card

Spectral expanders are edge expanders Arora and Barak, Section 21.2: in a d-regular graph, at least (1 - λ(G)) d |S| / 2 edges leave a set S of at most half of the vertices.

theorem Cslib.RotationMap.mul_card_filter_ne_le_card_filter_ne_neighbor {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) {α : Type u_3} [DecidableEq α] (f : V → α) {c : α} (hc : ∀ (a : α), {v : V | f v = a}.card ≤ {v : V | f v = c}.card) : (1 - G.spectralExpansion) * ↑(Fintype.card D) * ↑{v : V | f v ≠ c}.card ≤ ↑{p : V × D | f p.1 ≠ f (G.neighbor p.1 p.2)}.card

Disagreement across an expander, for a most frequent label: if no label is taken by more vertices than c, at least (1 - λ(G)) d |{f ≠ c}| darts join two differently labelled vertices, whatever the number of labels. The darts leaving the set of the vertices labelled a number at least (1 - λ(G)) d |{f = a}| |{f ≠ a}| / n, and |{f ≠ a}| ≥ |{f ≠ c}| for every label a.