The Expander Mixing Lemma

For a d-regular λ-expander G on n vertices and vertex sets A, B, the number of edges between A and B is close to what one would expect in a random d-regular graph: $$ \left| e(A, B) - \frac{d}{n} |A| |B| \right| \le \lambda d \sqrt{|A| |B|}. $$

Main definitions

• norm_adj_matrix: the normalised adjacency matrix M = A / d.
• expander: G is a γ-expander when every eigenvalue of M other than 1 is at most γ in absolute value.
• e_AB: the number of ordered pairs in A × B joined by an edge.

Main statements

• eq_const_of_mulVec_eq: on a connected graph every 1-eigenvector of M is constant.
• eigval_eq_one_unique: consequently the eigenvalue 1 is simple.
• expander_mixing_lemma: the inequality above.

References

• Swastik Kopparty, Lecture 2: Expander Graphs, Mixing lemma and Applications to randomness, Topics in Pseudo-randomness and Complexity Theory (Spring 2018), Rutgers University. Scribes: Danny Scheinerman, Harsha Tirumala.

noncomputable def norm_adj_matrix {V : Type u} (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) : Matrix V V ℝ

The normalized adjacency matrix M = A / d. Since G is d-regular, M is the transition matrix of the simple random walk on G, so its eigenvalues all lie in [-1, 1].

Equations

• norm_adj_matrix G d = (↑d)⁻¹ • SimpleGraph.adjMatrix ℝ G

theorem norm_adj_matrix_isHermitian {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] : (norm_adj_matrix G d).IsHermitian

M is symmetric (real symmetric matrices are Hermitian), so the spectral theorem applies.

theorem norm_adj_matrix_mulVec_const {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] (a : ℝ) : (norm_adj_matrix G d).mulVec (Function.const V a) = Function.const V a

Every constant function is a 1-eigenvector of M: since G is d-regular, every vertex has exactly d neighbours, so averaging a constant over them returns the same constant.

The eigenvalue 1 and its eigenspace

The mixing lemma's proof needs to know that the eigenvalue 1 of M is simple, with the constant function spanning its eigenspace. This is where connectivity of G enters: the argument below propagates the maximum of an eigenvector along walks.

theorem sum_neighbors_eq_of_mulVec_eq {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] {f : V → ℝ} (hf : (norm_adj_matrix G d).mulVec f = f) (v : V) : ∑ u ∈ G.neighborFinset v, f u = ↑d * f v

A 1-eigenvector f of M satisfies the mean-value property: its value at v is the average of its values over the d neighbours of v.

theorem eq_of_adj_of_isMax {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] {f : V → ℝ} {m : ℝ} (hf : (norm_adj_matrix G d).mulVec f = f) (hmax : ∀ (w : V), f w ≤ m) {v : V} (hv : f v = m) {u : V} (hadj : G.Adj v u) : f u = m

Maximum propagation. If a 1-eigenvector attains its global maximum m at v, then it equals m at every neighbour of v.

The point is that f v is the average of the d neighbouring values, all of which are ≤ m. An average of values ≤ m can only equal m if every one of them equals m.

theorem eq_of_walk_of_isMax {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] {f : V → ℝ} {m : ℝ} (hf : (norm_adj_matrix G d).mulVec f = f) (hmax : ∀ (w : V), f w ≤ m) {v w : V} (p : G.Walk v w) (hv : f v = m) : f w = m

The maximum spreads along any walk, so a 1-eigenvector is constant on each connected component.

theorem eq_const_of_mulVec_eq {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {d : ℕ} (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] {f : V → ℝ} (hconn : G.Connected) (hf : (norm_adj_matrix G d).mulVec f = f) : ∃ (c : ℝ), f = Function.const V c

The eigenvalue 1 of M is simple on a connected graph: every 1-eigenvector is constant. Together with norm_adj_matrix_mulVec_const this pins the eigenspace down exactly.

The spectrum of M and the definition of an expander

noncomputable def eigval {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] (i : V) : ℝ

The eigenvalues of M, indexed by the vertex set.

Equations

• eigval G d i = ⋯.eigenvalues i

noncomputable def eigvec {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] : OrthonormalBasis V ℝ (EuclideanSpace ℝ V)

A fixed orthonormal basis of eigenvectors of M, indexed by the vertex set.

Equations

• eigvec G d = ⋯.eigenvectorBasis

theorem mulVec_eigvec {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] (i : V) : (norm_adj_matrix G d).mulVec ((eigvec G d) i).ofLp = eigval G d i • ((eigvec G d) i).ofLp

theorem exists_eigval_eq_one {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] [Nonempty V] : ∃ (i : V), eigval G d i = 1

1 is an eigenvalue of M, witnessed by the constant eigenvector.

theorem card_mul_sq_eq_one {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] {i : V} {c : ℝ} (hc : ((eigvec G d) i).ofLp = Function.const V c) : ↑(Fintype.card V) * c ^ 2 = 1

Normalisation: a constant eigenvector has unit length, so n · c² = 1. This is the v₁ = 𝟙/√n of the informal proof, stated so that no square root — and no choice of sign — is ever needed.

theorem eigvec_const_of_eigval_eq_one {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] (hconn : G.Connected) {i : V} (hi : eigval G d i = 1) : ∃ (c : ℝ), c ≠ 0 ∧ ((eigvec G d) i).ofLp = Function.const V c

At an index carrying the eigenvalue 1, the eigenvector is a nonzero constant.

theorem eigval_eq_one_unique {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] (hconn : G.Connected) {i j : V} (hi : eigval G d i = 1) (hj : eigval G d j = 1) : i = j

The eigenvalue 1 is simple. Two distinct eigenbasis indices cannot both carry the eigenvalue 1: their eigenvectors would both be nonzero constants, hence not orthogonal.

def expander {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] (γ : ℝ) : Prop

G is a γ-expander when every eigenvalue of M other than the top eigenvalue 1 is at most γ in absolute value.

On a connected d-regular graph the eigenvalue 1 is simple (see eigval_eq_one_unique), so this really does exclude exactly one eigenvalue, as in the informal statement.

Equations

• expander G d γ = ∀ (i : V), eigval G d i ≠ 1 → |eigval G d i| ≤ γ

Expansion in the eigenbasis

The two identities below are the engine of the mixing lemma: the first is the informal proof's ⟨𝟙_A, M𝟙_B⟩ = ∑ αᵢβᵢλᵢ, the second is Parseval's ∑ αᵢ² = ‖𝟙_A‖².

theorem mulVec_eq_sum_eigvec {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] (y : EuclideanSpace ℝ V) : (norm_adj_matrix G d).mulVec y.ofLp = ∑ i : V, (eigval G d i * inner ℝ ((eigvec G d) i) y) • ((eigvec G d) i).ofLp

Applying M to a vector expanded in the eigenbasis scales each coordinate by λᵢ.

theorem dotProduct_mulVec_eq_sum {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] (x y : EuclideanSpace ℝ V) : x.ofLp ⬝ᵥ (norm_adj_matrix G d).mulVec y.ofLp = ∑ i : V, eigval G d i * inner ℝ ((eigvec G d) i) x * inner ℝ ((eigvec G d) i) y

⟨x, M y⟩ = ∑ᵢ λᵢ αᵢ βᵢ, where αᵢ = ⟨vᵢ, x⟩ and βᵢ = ⟨vᵢ, y⟩.

theorem sum_sq_inner_eq {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] (x : EuclideanSpace ℝ V) : ∑ i : V, inner ℝ ((eigvec G d) i) x ^ 2 = x.ofLp ⬝ᵥ x.ofLp

Parseval. The eigen-coefficients of x have the same total square as x itself.

def indicator {V : Type u} (S : Set V) [DecidablePred fun (x : V) => x ∈ S] : V → ℝ

Equations

• indicator S v = if v ∈ S then 1 else 0

def e_AB {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (A B : Set V) [DecidablePred fun (x : V) => x ∈ A] [DecidablePred fun (x : V) => x ∈ B] : ℕ

e(A, B) counts ordered pairs (a, b) ∈ A × B joined by an edge of G.

Equations

• e_AB G A B = {p : V × V | p.1 ∈ A ∧ p.2 ∈ B ∧ G.Adj p.1 p.2}.card

theorem e_AB_eq_sum_indicators {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (A B : Set V) [DecidablePred fun (x : V) => x ∈ A] [DecidablePred fun (x : V) => x ∈ B] : ↑(e_AB G A B) = ∑ i : V, ∑ j : V, indicator A i * indicator B j * SimpleGraph.adjMatrix ℝ G i j

def ind {V : Type u} (S : Set V) [DecidablePred fun (x : V) => x ∈ S] : EuclideanSpace ℝ V

𝟙_S viewed in EuclideanSpace, so that inner products against the eigenbasis are available.

Equations

• ind S = WithLp.toLp 2 (indicator S)

@[simp]

theorem ofLp_ind {V : Type u} [Fintype V] [DecidableEq V] (A : Set V) [DecidablePred fun (x : V) => x ∈ A] : (ind A).ofLp = indicator A

theorem sum_indicator {V : Type u} [Fintype V] [DecidableEq V] (A : Set V) [DecidablePred fun (x : V) => x ∈ A] : ∑ v : V, indicator A v = ↑A.toFinset.card

theorem dotProduct_ind_self {V : Type u} [Fintype V] [DecidableEq V] (A : Set V) [DecidablePred fun (x : V) => x ∈ A] : (ind A).ofLp ⬝ᵥ (ind A).ofLp = ↑A.toFinset.card

‖𝟙_A‖² = |A|, since the indicator is idempotent.

theorem e_AB_eq_dotProduct {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] (A B : Set V) [DecidablePred fun (x : V) => x ∈ A] [DecidablePred fun (x : V) => x ∈ B] : ↑(e_AB G A B) = ↑d * (ind A).ofLp ⬝ᵥ (norm_adj_matrix G d).mulVec (ind B).ofLp

e(A, B) = d ⟨𝟙_A, M 𝟙_B⟩, the first line of the informal computation.

theorem inner_eigvec_ind {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] (A : Set V) [DecidablePred fun (x : V) => x ∈ A] {i : V} {c : ℝ} (hc : ((eigvec G d) i).ofLp = Function.const V c) : inner ℝ ((eigvec G d) i) (ind A) = c * ↑A.toFinset.card

The coefficient of 𝟙_A along a constant eigenvector of value c is c · |A|. This is the informal proof's α₁ = ⟨𝟙_A, v₁⟩ = |A|/√n.

theorem sum_sq_inner_ind {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) [Fact (1 ≤ d)] (A : Set V) [DecidablePred fun (x : V) => x ∈ A] : ∑ i : V, inner ℝ ((eigvec G d) i) (ind A) ^ 2 = ↑A.toFinset.card

Parseval, specialised to an indicator: ∑ᵢ αᵢ² = |A|.

theorem expander_mixing_lemma {V : Type u} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (d : ℕ) (h_reg : G.IsRegularOfDegree d) [Fact (1 ≤ d)] (A B : Set V) [DecidablePred fun (x : V) => x ∈ A] [DecidablePred fun (x : V) => x ∈ B] (hconn : G.Connected) (γ : ℝ) (hγ : 0 ≤ γ) (hexp : expander G d γ) : |↑(e_AB G A B) - ↑d / ↑(Fintype.card V) * ↑A.toFinset.card * ↑B.toFinset.card| ≤ γ * ↑d * √(↑A.toFinset.card * ↑B.toFinset.card)

Expander mixing lemma. For a connected d-regular γ-expander on n = |V| vertices and any two sets of vertices A, B, $$ \left| e(A,B) - \frac{d}{n}|A||B| \right| \le \gamma\, d \sqrt{|A||B|}. $$

The estimate e(A,B) ≈ (d/n)|A||B| is what one expects for a random d-regular graph.