Definition 18: Cheeger Constant

The Cheeger constant of a finite graph G, viewed as a 1-dimensional cell complex (Def_7), is h(G) = min_{S} |δS| / |S| where the minimum is over nonempty subsets S ⊆ V with 2|S| ≤ |V|, and δS is the edge boundary of S.

Main Results

• edgeBoundary — the edge boundary δS
• mem_edgeBoundary — membership characterization
• EligibleSubset — eligible subsets for the Cheeger constant
• isoperimetricRatio — the ratio |δS| / |S|
• cheegerConstant — the Cheeger constant h(G)
• eligibleSubset_nonempty — eligible subsets exist when |V| ≥ 2
• cheegerConstant_nonneg — h(G) ≥ 0
• cheegerInequalities — the Cheeger inequalities relating h(G) to the spectral gap

Edge Boundary

noncomputable def CheegerConstant.edgeBoundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset (Sym2 V)

The edge boundary δS = {{u,v} ∈ E(G) | u ∈ S, v ∉ S} of a vertex subset S. An edge is in δS iff it has one endpoint in S and one endpoint outside S. By the symmetry of Sym2, it suffices to check that there exist a ∈ S, b ∉ S with e = s(a, b).

Equations

• CheegerConstant.edgeBoundary G S = {e ∈ G.edgeFinset | (Quot.out e).1 ∈ S ∧ (Quot.out e).2 ∉ S ∨ (Quot.out e).2 ∈ S ∧ (Quot.out e).1 ∉ S}

theorem CheegerConstant.mem_edgeBoundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (e : Sym2 V) : e ∈ edgeBoundary G S ↔ e ∈ G.edgeFinset ∧ ∃ (a : V) (b : V), s(a, b) = e ∧ a ∈ S ∧ b ∉ S

Membership in the edge boundary: e ∈ δS iff e is an edge of G and there exist a ∈ S, b ∉ S with e = s(a, b).

theorem CheegerConstant.edgeBoundary_subset_edgeFinset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : edgeBoundary G S ⊆ G.edgeFinset

The edge boundary is a subset of the edge set.

theorem CheegerConstant.adj_mem_edgeBoundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) {u v : V} (hadj : G.Adj u v) (hu : u ∈ S) (hv : v ∉ S) : s(u, v) ∈ edgeBoundary G S

An edge {u, v} with u ∈ S and v ∉ S is in the edge boundary.

Eligible Subsets and Isoperimetric Ratio

def CheegerConstant.EligibleSubset {V : Type u_1} [Fintype V] (S : Finset V) : Prop

The eligible subsets for the Cheeger constant: nonempty subsets S ⊆ V with 2|S| ≤ |V|. The paper uses strict inequality |S| < |V|/2 in one place, but |S| ≤ |V|/2 elsewhere; the standard convention is 2|S| ≤ |V|.

Equations

• CheegerConstant.EligibleSubset S = (S.Nonempty ∧ 2 * S.card ≤ Fintype.card V)

noncomputable def CheegerConstant.isoperimetricRatio {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : ℝ

The isoperimetric ratio |δS| / |S| for a subset S.

Equations

• CheegerConstant.isoperimetricRatio G S = ↑(CheegerConstant.edgeBoundary G S).card / ↑S.card

noncomputable def CheegerConstant.cheegerConstant {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℝ

The Cheeger constant h(G) = inf_{S} |δS| / |S| where the infimum is over nonempty subsets S ⊆ V with 2|S| ≤ |V|. When no eligible subset exists (e.g., |V| < 2), the value is 0 by the convention sInf ∅ = 0 for ℝ.

Equations

• CheegerConstant.cheegerConstant G = sInf {r : ℝ | ∃ (S : Finset V), CheegerConstant.EligibleSubset S ∧ CheegerConstant.isoperimetricRatio G S = r}

Eligible Subsets Exist

theorem CheegerConstant.eligibleSubset_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] (hcard : 2 ≤ Fintype.card V) : ∃ (S : Finset V), EligibleSubset S

When |V| ≥ 2, there exists an eligible subset (any singleton).

Cheeger Constant is Nonneg

theorem CheegerConstant.cheegerConstant_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : 0 ≤ cheegerConstant G

The Cheeger constant is nonneg: 0 ≤ h(G).

Cheeger Inequalities

axiom cheegerInequalities {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hcard : 2 ≤ Fintype.card V) (hconn : G.Connected) (hreg : G.IsRegularOfDegree s) : let lam2 := GraphExpansion.secondLargestEigenvalue G hcard; let hG := CheegerConstant.cheegerConstant G; (↑s - lam2) / 2 ≤ hG ∧ hG ≤ √(2 * ↑s * (↑s - lam2))

The Cheeger inequalities for a connected s-regular graph G with second-largest adjacency eigenvalue λ₂ (Def_14) state that (s - λ₂)/2 ≤ h(G) ≤ √(2s(s - λ₂)).

The lower bound (s - λ₂)/2 ≤ h(G) follows from the variational characterization of λ₂ (Courant–Fischer), and the upper bound h(G) ≤ √(2s(s - λ₂)) from the sweep-cut argument on the second eigenvector.

This is stated as an axiom because the proof requires spectral theory infrastructure (Courant–Fischer min-max theorem, sweep-cut analysis) not available in Mathlib.