Cheeger's inequality: edge expansion gives a spectral gap

EdgeExpansion proved that a spectral gap forces every set to have many boundary darts. This module proves the converse — the harder direction of Cheeger's inequality — in the form the rest of the development consumes: a SpectralBound below one, for the graph with a self-loop added per dart.

The argument is the classical one, made discrete.

• The Dirichlet form ∑ (f u - f w)² over darts equals 2 d (‖f‖² - ⟨f, step f⟩).
• Co-area. For ψ ≥ 0 supported on at most half the vertices, ∑ |ψ u - ψ w| ≥ 2 h d ∑ ψ: peel off the lowest positive level, apply the expansion to the support, and induct on the support.
• Cauchy–Schwarz turns the co-area bound for ψ = φ² into h² d ∑ φ² ≤ Dirichlet φ for nonnegative φ of small support.
• A median split extends this to every mean-zero f, losing nothing.
• The lazy walk. Adding d loops halves the step operator plus the identity, which is positive semidefinite, and a Cauchy–Schwarz for semidefinite forms turns the Rayleigh bound into an operator bound — no spectral theorem needed.

Main definitions

• Complexity.RegGraph.EdgeExpansion — every set of at most half the vertices has at least h d |S| boundary darts
• Complexity.RegGraph.dirichlet — the Dirichlet form over darts

Main results

• Complexity.RegGraph.dirichlet_ge_of_edgeExpansion — h² d ‖f‖² ≤ Dirichlet f for mean-zero f
• Complexity.RegGraph.spectralBound_padLoops_of_edgeExpansion — the lazy graph has bound 1 - h² / 4

Darts and their reversal

def Complexity.RegGraph.rotPerm (G : RegGraph) : Equiv.Perm (G.V × G.D)

The reversal of darts, as a permutation.

Equations

• G.rotPerm = Function.Involutive.toPerm G.rot ⋯

theorem Complexity.RegGraph.nbr_rot (G : RegGraph) (p : G.V × G.D) : G.nbr (G.rot p).1 (G.rot p).2 = p.1

theorem Complexity.RegGraph.sum_darts_swap (G : RegGraph) (g : G.V → G.V → ℝ) : ∑ p : G.V × G.D, g p.1 (G.nbr p.1 p.2) = ∑ p : G.V × G.D, g (G.nbr p.1 p.2) p.1

Reversing every dart swaps the two ends in a sum.

theorem Complexity.RegGraph.sum_darts_fst (G : RegGraph) (g : G.V → ℝ) : ∑ p : G.V × G.D, g p.1 = ↑G.deg * ∑ v : G.V, g v

theorem Complexity.RegGraph.sum_darts_snd (G : RegGraph) (g : G.V → ℝ) : ∑ p : G.V × G.D, g (G.nbr p.1 p.2) = ↑G.deg * ∑ v : G.V, g v

theorem Complexity.RegGraph.sum_mul_step (G : RegGraph) (f g : G.V → ℝ) : ∑ v : G.V, f v * G.step g v = (∑ p : G.V × G.D, f p.1 * g (G.nbr p.1 p.2)) / ↑G.deg

Edge expansion and the Dirichlet form

def Complexity.RegGraph.EdgeExpansion (G : RegGraph) (h : ℝ) : Prop

Edge expansion: every set of at most half the vertices has at least h · d · |S| darts leaving it.

Equations

• G.EdgeExpansion h = ∀ (S : Finset G.V), 2 * S.card ≤ G.order → h * ↑G.deg * ↑S.card ≤ ↑(G.dartsBetween S Sᶜ).card

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

The Dirichlet form: the sum over darts of the squared difference.

Equations

• G.dirichlet f = ∑ p : G.V × G.D, (f p.1 - f (G.nbr p.1 p.2)) ^ 2

theorem Complexity.RegGraph.dirichlet_nonneg (G : RegGraph) (f : G.V → ℝ) : 0 ≤ G.dirichlet f

theorem Complexity.RegGraph.dirichlet_eq (G : RegGraph) (f : G.V → ℝ) : G.dirichlet f = 2 * ↑G.deg * (∑ v : G.V, f v ^ 2 - ∑ v : G.V, f v * G.step f v)

The Dirichlet form and the step operator.

theorem Complexity.RegGraph.dirichlet_sub_const (G : RegGraph) (f : G.V → ℝ) (c : ℝ) : (G.dirichlet fun (v : G.V) => f v - c) = G.dirichlet f

The Dirichlet form is invariant under adding a constant.

Co-area

theorem Complexity.RegGraph.sum_darts_boundary (G : RegGraph) (S : Finset G.V) : ((∑ p : G.V × G.D, if p.1 ∈ S ∧ G.nbr p.1 p.2 ∉ S then 1 else 0) + ∑ p : G.V × G.D, if p.1 ∉ S ∧ G.nbr p.1 p.2 ∈ S then 1 else 0) = 2 * ↑(G.dartsBetween S Sᶜ).card

The darts crossing out of or into S, counted with the boundary in both directions.

noncomputable def Complexity.RegGraph.support (G : RegGraph) (ψ : G.V → ℝ) : Finset G.V

The support of a function.

Equations

• G.support ψ = {v : G.V | ψ v ≠ 0}

theorem Complexity.RegGraph.mem_support_iff (G : RegGraph) (ψ : G.V → ℝ) (v : G.V) : v ∈ G.support ψ ↔ ψ v ≠ 0

theorem Complexity.RegGraph.eq_zero_of_notMem_support (G : RegGraph) (ψ : G.V → ℝ) {v : G.V} (hv : v ∉ G.support ψ) : ψ v = 0

theorem Complexity.RegGraph.coarea (G : RegGraph) {h : ℝ} (hexp : G.EdgeExpansion h) (n : ℕ) (ψ : G.V → ℝ) : (G.support ψ).card = n → (∀ (v : G.V), 0 ≤ ψ v) → 2 * (G.support ψ).card ≤ G.order → 2 * h * ↑G.deg * ∑ v : G.V, ψ v ≤ ∑ p : G.V × G.D, |ψ p.1 - ψ (G.nbr p.1 p.2)|

Co-area. For ψ ≥ 0 supported on at most half the vertices, ∑ |ψ u - ψ w| ≥ 2 h d ∑ ψ.

The core bound for small support

theorem Complexity.RegGraph.support_sq (G : RegGraph) (φ : G.V → ℝ) : (G.support fun (v : G.V) => φ v ^ 2) = G.support φ

theorem Complexity.RegGraph.dirichlet_ge_of_support (G : RegGraph) {h : ℝ} (hexp : G.EdgeExpansion h) (hh : 0 ≤ h) (φ : G.V → ℝ) (hpos : ∀ (v : G.V), 0 ≤ φ v) (hhalf : 2 * (G.support φ).card ≤ G.order) : h ^ 2 * ↑G.deg * ∑ v : G.V, φ v ^ 2 ≤ G.dirichlet φ

Small support. For φ ≥ 0 supported on at most half the vertices, h² d ‖φ‖² ≤ Dirichlet φ.

The median split

theorem Complexity.RegGraph.exists_median (G : RegGraph) (f : G.V → ℝ) : ∃ (c : ℝ), 2 * {v : G.V | c < f v}.card ≤ G.order ∧ 2 * {v : G.V | f v < c}.card ≤ G.order

A median. Some value has at most half the vertices strictly above it and at most half strictly below.

theorem Complexity.RegGraph.support_max_subset (G : RegGraph) (g : G.V → ℝ) : (G.support fun (v : G.V) => max (g v) 0) ⊆ {v : G.V | 0 < g v}

theorem Complexity.RegGraph.dirichlet_ge_of_edgeExpansion (G : RegGraph) {h : ℝ} (hexp : G.EdgeExpansion h) (hh : 0 ≤ h) (f : G.V → ℝ) (hf : ∑ v : G.V, f v = 0) : h ^ 2 * ↑G.deg * ∑ v : G.V, f v ^ 2 ≤ G.dirichlet f

Cheeger's inequality, Dirichlet form. For mean-zero f, h² d ‖f‖² ≤ Dirichlet f.

The lazy walk

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

The lazy quadratic form, as an inner product of dart sums.

Equations

• G.lazyQ f g = ∑ p : G.V × G.D, (f p.1 + f (G.nbr p.1 p.2)) * (g p.1 + g (G.nbr p.1 p.2))

theorem Complexity.RegGraph.step_lazy (G : RegGraph) (f : G.V → ℝ) (v : G.V) : (G.padLoops G.deg).step f v = (G.step f v + f v) / 2

theorem Complexity.RegGraph.sum_lazy_mul (G : RegGraph) (f g : G.V → ℝ) : ∑ v : G.V, (G.padLoops G.deg).step f v * g v = G.lazyQ f g / (4 * ↑G.deg)

The lazy step against a function is the lazy form.

theorem Complexity.RegGraph.lazyQ_self (G : RegGraph) (f : G.V → ℝ) : G.lazyQ f f = 4 * ↑G.deg * ∑ v : G.V, f v ^ 2 - G.dirichlet f

theorem Complexity.RegGraph.lazyQ_nonneg (G : RegGraph) (f : G.V → ℝ) : 0 ≤ G.lazyQ f f

theorem Complexity.RegGraph.lazyQ_sq_le (G : RegGraph) (f g : G.V → ℝ) : G.lazyQ f g ^ 2 ≤ G.lazyQ f f * G.lazyQ g g

theorem Complexity.RegGraph.sum_lazy_step (G : RegGraph) (f : G.V → ℝ) : ∑ v : G.V, (G.padLoops G.deg).step f v = ∑ v : G.V, f v

theorem Complexity.RegGraph.spectralBound_padLoops_of_edgeExpansion (G : RegGraph) {h : ℝ} (hexp : G.EdgeExpansion h) (hh : 0 ≤ h) : (G.padLoops G.deg).SpectralBound (1 - h ^ 2 / 4)

Cheeger's inequality, spectral form. Edge expansion h gives the lazy graph — d self-loops added — the spectral bound 1 - h² / 4.