Cheeger's inequality for regular graphs

The edge expansion h(G) of a regular graph measures combinatorially how well it is connected: it is the least number of edges leaving a set of at most half of the vertices, per vertex of the set. Its spectral counterpart is the gap 1 - λ₂(G) between the two largest eigenvalues of the walk operator. The discrete Cheeger inequality Hoory, Linial and Wigderson, Theorem 2.4 Arora and Barak, Section 21.2 says that the two agree up to a square: for a d-regular graph,

d (1 - λ₂(G)) / 2 ≤ h(G) ≤ d √(2 (1 - λ₂(G))).

The edge expansion h(G) (edgeExpansion) is normalized as in Hoory, Linial and Wigderson, Definition 2.1: it is the minimum of e(S, Sᶜ) / |S| over the nonempty sets S of at most half of the vertices, where e(S, Sᶜ) counts the edges between S and its complement; Arora and Barak, Section 21.2 divides it by d. The second eigenvalue λ₂(G) (secondEigenvalue) is the supremum of the Rayleigh quotient 𝔼 f · G.walk f / 𝔼 f² over the nonzero functions f of expectation zero. It lies between -λ(G) and λ(G), and equals the spectral expansion λ(G) when the walk operator is positive semidefinite. Both are defined without spectral theory and used through their characterizations secondEigenvalue_le_iff and le_edgeExpansion_iff; on fewer than two vertices both are 0 by convention.

The easy half is the one-sided expander mixing lemma le_card_interedges_compl_of_expect_mul_walk_le. The hard half is proved for every function f of expectation zero, with no eigenvector. Over a uniformly random dart (u, w), the Dirichlet form 𝔼 (f u - f w)² is 2 (𝔼 f² - 𝔼 f · G.walk f), and it does not change when f is shifted by a constant. Shifted by a median, f splits into a positive and a negative part, each vanishing outside a set of at most half of the vertices. For such a nonnegative φ, the co-area inequality bounds the variation of φ² along the darts from below by the edges leaving the level sets of φ, and the Cauchy–Schwarz inequality turns this into h(G)² 𝔼 φ² ≤ d² 𝔼 (φ u - φ w)².

Edge expansion bounds λ₂(G) but not λ(G): a bipartite graph can be a good edge expander, yet -1 is an eigenvalue of its walk operator. The lazy walk (f + G.walk f) / 2, which stays put with probability 1 / 2, is positive semidefinite, so a rotation map with this walk operator has spectral expansion at most 1 - h(G)² / (4 d²).

Main definitions

• Cslib.RotationMap.secondEigenvalue: the second eigenvalue λ₂(G) of the walk operator.
• Cslib.RotationMap.edgeExpansion: the edge expansion h(G).

Main results

• Cslib.RotationMap.secondEigenvalue_le_iff, Cslib.RotationMap.le_edgeExpansion_iff: the characterizations of λ₂(G) and h(G).
• Cslib.RotationMap.edgeExpansion_mul_card_div_three_le_card_interedges: at least h(G) |V| / 3 edges leave every set of between a third and two thirds of the vertices.
• Cslib.RotationMap.abs_secondEigenvalue_le_spectralExpansion: |λ₂(G)| ≤ λ(G).
• Cslib.RotationMap.spectralExpansion_eq_secondEigenvalue_of_nonneg: λ(G) = λ₂(G) when the walk operator is positive semidefinite.
• Cslib.RotationMap.card_mul_one_sub_secondEigenvalue_div_two_le_edgeExpansion: the easy half of Cheeger's inequality.
• Cslib.RotationMap.expect_mul_walk_le_of_mul_card_le_card_interedges_compl: the hard half of Cheeger's inequality in one-sided form, from any lower bound on the edges leaving small sets.
• Cslib.RotationMap.edgeExpansion_le_card_mul_sqrt, Cslib.RotationMap.secondEigenvalue_le_one_sub_edgeExpansion_sq_div: the hard half of Cheeger's inequality.
• Cslib.RotationMap.spectralExpansion_le_one_sub_edgeExpansion_sq_div: edge expansion bounds the spectral expansion of the lazy walk.

References

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

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

The second eigenvalue λ₂(G) of the walk operator: the supremum of the Rayleigh quotient 𝔼 v, f v * G.walk f v / 𝔼 v, f v ^ 2 over the nonzero functions f of expectation zero, that is over the nonzero functions orthogonal to the constants. When V has at most one vertex there is no such function, and λ₂(G) = 0 by convention. Otherwise, as the walk operator is self-adjoint and fixes the constants, this is its second largest eigenvalue counted with multiplicity, but nothing here depends on that: λ₂(G) is used through expect_mul_walk_le_secondEigenvalue_mul and secondEigenvalue_le_iff.

theorem Cslib.RotationMap.expect_mul_walk_le_secondEigenvalue_mul {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.secondEigenvalue * Finset.univ.expect fun (v : V) => f v ^ 2

For f of expectation zero, 𝔼 v, f v * G.walk f v ≤ λ₂(G) 𝔼 f².

theorem Cslib.RotationMap.secondEigenvalue_le_iff {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [Nontrivial V] {μ : ℝ} : G.secondEigenvalue ≤ μ ↔ ∀ (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

On at least two vertices, λ₂(G) ≤ μ exactly when 𝔼 v, f v * G.walk f v ≤ μ 𝔼 f² for every function f of expectation zero.

theorem Cslib.RotationMap.secondEigenvalue_eq_zero_of_subsingleton {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [Subsingleton V] : G.secondEigenvalue = 0

On at most one vertex, λ₂(G) = 0 by convention.

theorem Cslib.RotationMap.secondEigenvalue_le_spectralExpansion {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) : G.secondEigenvalue ≤ G.spectralExpansion

The second eigenvalue is at most the spectral expansion.

theorem Cslib.RotationMap.neg_spectralExpansion_le_secondEigenvalue {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) : -G.spectralExpansion ≤ G.secondEigenvalue

The second eigenvalue is at least minus the spectral expansion.

theorem Cslib.RotationMap.abs_secondEigenvalue_le_spectralExpansion {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) : |G.secondEigenvalue| ≤ G.spectralExpansion

The second eigenvalue is at most the spectral expansion in absolute value.

theorem Cslib.RotationMap.secondEigenvalue_le_one {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) : G.secondEigenvalue ≤ 1

The second eigenvalue is at most one.

theorem Cslib.RotationMap.neg_one_le_secondEigenvalue {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) : -1 ≤ G.secondEigenvalue

The second eigenvalue is at least minus one.

theorem Cslib.RotationMap.spectralExpansion_eq_secondEigenvalue_of_nonneg {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) (h : ∀ (f : V → ℝ), 0 ≤ Finset.univ.expect fun (v : V) => f v * G.walk f v) : G.spectralExpansion = G.secondEigenvalue

If the walk operator is positive semidefinite, 0 ≤ 𝔼 v, f v * G.walk f v for every f, then the spectral expansion is the second eigenvalue: λ(G) = λ₂(G).

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

The edge expansion h(G) Hoory, Linial and Wigderson, Definition 2.1: the least ratio e(S, Sᶜ) / |S| of the number e(S, Sᶜ) of edges leaving S to the size of S, over the nonempty sets S of at most half of the vertices. It counts edges, so 0 ≤ h(G) ≤ |D|; Arora and Barak, Section 21.2 divides it by the degree |D| instead. When V has at most one vertex there is no such set, and h(G) = 0 by convention.

theorem Cslib.RotationMap.edgeExpansion_nonneg {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] : 0 ≤ G.edgeExpansion

The edge expansion is nonnegative.

theorem Cslib.RotationMap.edgeExpansion_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) : G.edgeExpansion * ↑S.card ≤ ↑(G.interedges S Sᶜ).card

At least h(G) |S| edges leave every set S of at most half of the vertices.

theorem Cslib.RotationMap.le_edgeExpansion_iff {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] [Nontrivial V] {c : ℝ} : c ≤ G.edgeExpansion ↔ ∀ (S : Finset V), 2 * S.card ≤ Fintype.card V → c * ↑S.card ≤ ↑(G.interedges S Sᶜ).card

On at least two vertices, c ≤ h(G) exactly when at least c |S| edges leave every set S of at most half of the vertices.

theorem Cslib.RotationMap.edgeExpansion_eq_zero_of_subsingleton {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] [Subsingleton V] : G.edgeExpansion = 0

On at most one vertex, h(G) = 0 by convention.

theorem Cslib.RotationMap.edgeExpansion_le_card {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] : G.edgeExpansion ≤ ↑(Fintype.card D)

The edge expansion is at most the degree |D|.

theorem Cslib.RotationMap.edgeExpansion_mul_card_div_three_le_card_interedges {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] {S : Finset V} (h₁ : Fintype.card V ≤ 3 * S.card) (h₂ : 3 * S.card ≤ 2 * Fintype.card V) : G.edgeExpansion * ↑(Fintype.card V) / 3 ≤ ↑(G.interedges S Sᶜ).card

At least h(G) |V| / 3 edges leave every set of between a third and two thirds of the vertices: the set, or its complement, has at most half and at least a third of the vertices.

theorem Cslib.RotationMap.card_mul_one_sub_secondEigenvalue_div_two_le_edgeExpansion {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] [Nontrivial V] : ↑(Fintype.card D) * (1 - G.secondEigenvalue) / 2 ≤ G.edgeExpansion

The easy half of Cheeger's inequality Hoory, Linial and Wigderson, Theorem 2.4 Arora and Barak, Section 21.2: on at least two vertices, |D| (1 - λ₂(G)) / 2 ≤ h(G).

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

Edge expansion bounds the second eigenvalue Hoory, Linial and Wigderson, Theorem 2.4 Arora and Barak, Section 21.2: if c ≥ 0 and at least c |S| edges leave every set S of at most half of the vertices, then 𝔼 v, f v * G.walk f v ≤ (1 - c ^ 2 / (2 |D| ^ 2)) 𝔼 f² for every f of expectation zero. This is the hard half of the discrete Cheeger inequality in one-sided form, converse to le_card_interedges_compl_of_expect_mul_walk_le.

theorem Cslib.RotationMap.secondEigenvalue_le_one_sub_edgeExpansion_sq_div {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] : G.secondEigenvalue ≤ 1 - G.edgeExpansion ^ 2 / (2 * ↑(Fintype.card D) ^ 2)

The hard half of Cheeger's inequality Hoory, Linial and Wigderson, Theorem 2.4 Arora and Barak, Section 21.2, as a bound on the second eigenvalue: λ₂(G) ≤ 1 - h(G) ^ 2 / (2 |D| ^ 2).

theorem Cslib.RotationMap.edgeExpansion_sq_le {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] : G.edgeExpansion ^ 2 ≤ 2 * ↑(Fintype.card D) ^ 2 * (1 - G.secondEigenvalue)

The hard half of Cheeger's inequality Hoory, Linial and Wigderson, Theorem 2.4 Arora and Barak, Section 21.2, squared: h(G) ^ 2 ≤ 2 |D| ^ 2 (1 - λ₂(G)).

theorem Cslib.RotationMap.edgeExpansion_le_card_mul_sqrt {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] : G.edgeExpansion ≤ ↑(Fintype.card D) * √(2 * (1 - G.secondEigenvalue))

The hard half of Cheeger's inequality Hoory, Linial and Wigderson, Theorem 2.4 Arora and Barak, Section 21.2: h(G) ≤ |D| √(2 (1 - λ₂(G))).

theorem Cslib.RotationMap.spectralExpansion_le_one_add_secondEigenvalue_div_two {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) {E : Type u_3} [Fintype E] (H : RotationMap V E) (hH : ∀ (f : V → ℝ) (v : V), H.walk f v = (f v + G.walk f v) / 2) : H.spectralExpansion ≤ (1 + G.secondEigenvalue) / 2

The spectral expansion of the lazy walk: if H.walk f v = (f v + G.walk f v) / 2 for all f and v, so that the walk on H stays put with probability 1 / 2 and otherwise takes a step of the walk on G, then λ(H) ≤ (1 + λ₂(G)) / 2. The walk operator of H is positive semidefinite, so its spectral expansion is its second eigenvalue.

theorem Cslib.RotationMap.spectralExpansion_le_one_sub_edgeExpansion_sq_div {V : Type u_1} {D : Type u_2} [Fintype V] [Fintype D] (G : RotationMap V D) [DecidableEq V] {E : Type u_3} [Fintype E] (H : RotationMap V E) (hH : ∀ (f : V → ℝ) (v : V), H.walk f v = (f v + G.walk f v) / 2) : H.spectralExpansion ≤ 1 - G.edgeExpansion ^ 2 / (4 * ↑(Fintype.card D) ^ 2)

Edge expansion bounds the spectral expansion of the lazy walk: if H.walk f v = (f v + G.walk f v) / 2 for all f and v, then λ(H) ≤ 1 - h(G) ^ 2 / (4 |D| ^ 2).