Lemma 1: Relative Cheeger Inequality

Main Results

• relativeCheeger: For a finite, connected, s-regular graph with second-largest eigenvalue λ₂, and for S ⊆ V with 0 < |S| < α|V| where α ∈ (0, 1), we have (1 - α)(s - λ₂) ≤ |δS| / |S|.

Step 0: Well-definedness

Since |S| ≥ 1 and |S| < α|V| with α < 1, we have |V| ≥ 2, so λ₂ is well-defined.

theorem RelativeCheeger.card_ge_two_of_subset {V : Type u_1} [Fintype V] [DecidableEq V] (S : Finset V) (α : ℝ) (hα1 : α < 1) (hS_pos : 0 < S.card) (hS_lt : ↑S.card < α * ↑(Fintype.card V)) : 2 ≤ Fintype.card V

Spectral Laplacian Bound (Axiom)

The key spectral theory fact: for a connected s-regular graph, the Laplacian quadratic form of the characteristic function of a proper nonempty subset S satisfies |δS| ≥ (s - λ₂) · |S| · (1 - |S|/|V|).

This combines Steps 1–4 of the proof:

• Step 1: Define f = 1_S, decompose f = f̄·1 + g
• Step 2: Spectral theorem gives gᵀ(sI-M)g ≥ (s-λ₂)·gᵀg
• Step 3: gᵀg = |S|·(1 - |S|/|V|), and fᵀ(sI-M)f = |δS|
• Step 4: gᵀ(sI-M)g = fᵀ(sI-M)f since (sI-M)·1 = 0

The proof requires eigenvalue decomposition and the Courant–Fischer variational characterization (not available in Mathlib), so this is stated as an axiom, following the same convention as cheegerInequalities in Def_18.

axiom RelativeCheeger.spectralLaplacianBound {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) (S : Finset V) (hS_pos : 0 < S.card) (hS_lt : S.card < Fintype.card V) : (↑s - GraphExpansion.secondLargestEigenvalue G hcard) * ↑S.card * (1 - ↑S.card / ↑(Fintype.card V)) ≤ ↑(CheegerConstant.edgeBoundary G S).card

theorem RelativeCheeger.spectralLaplacianBound_satisfiable {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hcard : 2 ≤ Fintype.card V) (hconn : G.Connected) : ∃ (S : Finset V), 0 < S.card ∧ S.card < Fintype.card V

Witness for spectralLaplacianBound: there exist S and V satisfying the hypotheses. Any connected graph on ≥ 2 vertices has a proper nonempty subset.

Step 5: Combining the bounds

theorem RelativeCheeger.card_div_lt_alpha {V : Type u_1} [Fintype V] [DecidableEq V] (S : Finset V) (α : ℝ) (hα0 : 0 < α) (hS_lt : ↑S.card < α * ↑(Fintype.card V)) (hV : 0 < Fintype.card V) : ↑S.card / ↑(Fintype.card V) < α

Helper: |S|/|V| < α when |S| < α·|V|.

theorem RelativeCheeger.card_lt_of_alpha {V : Type u_1} [Fintype V] [DecidableEq V] (S : Finset V) (α : ℝ) (hα1 : α < 1) (hS_lt : ↑S.card < α * ↑(Fintype.card V)) : S.card < Fintype.card V

Helper: S.card < Fintype.card V when (S.card : ℝ) < α * Fintype.card V and α < 1.

Main Theorem

theorem RelativeCheeger.relativeCheeger {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (α : ℝ) (hα0 : 0 < α) (hα1 : α < 1) (hconn : G.Connected) (hreg : G.IsRegularOfDegree s) (S : Finset V) (hS_pos : 0 < S.card) (hS_lt : ↑S.card < α * ↑(Fintype.card V)) : have hcard := ⋯; (1 - α) * (↑s - GraphExpansion.secondLargestEigenvalue G hcard) ≤ ↑(CheegerConstant.edgeBoundary G S).card / ↑S.card

Relative Cheeger Inequality. For a finite, connected, s-regular graph with second-largest eigenvalue λ₂, and for α ∈ (0, 1) and S ⊆ V with 0 < |S| < α|V|, we have (1 - α)(s - λ₂) ≤ |δS| / |S|.

This follows from the spectral Laplacian bound: |δS| ≥ (s - λ₂) · |S| · (1 - |S|/|V|) > (s - λ₂) · |S| · (1 - α) since |S|/|V| < α, and then dividing by |S| > 0.