25 Lem 1: Relative Cheeger Inequality

Lemma 287 Cardinality at Least Two from Subset Bound

✓

Let $V$ be a finite type, $S \subseteq V$ a finset, and $\alpha \in \mathbb {R}$ with $\alpha {\lt} 1$. If $0 {\lt} |S|$ and $|S| {\lt} \alpha \cdot |V|$, then $|V| \geq 2$.

Proof ▶

We argue by contradiction. Suppose $|V| {\lt} 2$. Since $|V|$ is a natural number, $|V| \leq 1$. Since $S \subseteq V$, we have $|S| \leq |V| \leq 1$, so combined with $0 {\lt} |S|$ we get $|S| = 1$ and thus $|V| = 1$. Substituting into $|S| {\lt} \alpha \cdot |V|$ yields $1 {\lt} \alpha \cdot 1 = \alpha $, but this contradicts $\alpha {\lt} 1$. Hence $|V| \geq 2$.

Theorem 288 Axiom: Spectral Laplacian Bound

✓

red[UNPROVEN AXIOM]

Let $G = (V, E)$ be a finite, connected, $s$-regular simple graph with $|V| \geq 2$, and let $\lambda _2$ denote its second-largest adjacency eigenvalue. For any nonempty proper subset $S \subsetneq V$ (i.e., $0 {\lt} |S| {\lt} |V|$), the edge boundary $\delta S$ satisfies:

\[ (s - \lambda _2) \cdot |S| \cdot \left(1 - \frac{|S|}{|V|}\right) \leq |\delta S|. \]

Note: This is stated as an axiom because the proof requires eigenvalue decomposition and the Courant–Fischer variational characterization of $\lambda _2$, which are not currently available in Mathlib. The proof strategy is: (Step 1) Set $f = \mathbf{1}_S$, decompose $f = \bar{f}\cdot \mathbf{1} + g$ where $\bar{f} = |S|/|V|$; (Step 2) By the spectral theorem, $g^\top (sI - M)g \geq (s - \lambda _2)\, g^\top g$; (Step 3) Compute $g^\top g = |S|(1 - |S|/|V|)$ and $f^\top (sI-M)f = |\delta S|$; (Step 4) Since $(sI-M)\cdot \mathbf{1} = 0$, we have $g^\top (sI-M)g = f^\top (sI-M)f$, completing the bound. This follows the same convention as cheegerInequalities in the Cheeger constant file.

Lemma 289 Satisfiability Witness for Spectral Laplacian Bound

✓

Let $G = (V, E)$ be a finite, connected simple graph with $|V| \geq 2$. Then there exists a finset $S \subseteq V$ with $0 {\lt} |S|$ and $|S| {\lt} |V|$, confirming that the hypotheses of the spectral Laplacian bound axiom are satisfiable.

Proof ▶

Since $|V| \geq 2 {\gt} 0$, the type $V$ is nonempty; obtain any vertex $v \in V$. Take $S = \{ v\} $. Then $|S| = 1 {\gt} 0$, and $|S| = 1 {\lt} |V|$ because $|V| \geq 2$. This provides the required witness.

Lemma 290 Card Ratio Less Than Alpha

✓

Let $S \subseteq V$ be a finset, $\alpha \in \mathbb {R}$ with $\alpha {\gt} 0$, and $|V| {\gt} 0$. If $|S| {\lt} \alpha \cdot |V|$, then $|S| / |V| {\lt} \alpha $.

Proof ▶

Since $|V| {\gt} 0$, we have $(|V| : \mathbb {R}) {\gt} 0$. Using the equivalence $|S|/|V| {\lt} \alpha \Leftrightarrow |S| {\lt} \alpha \cdot |V|$ (valid for positive $|V|$), the result follows directly from the hypothesis $|S| {\lt} \alpha \cdot |V|$ by dividing both sides by $|V|$.

Lemma 291 Card Strictly Less Than Total From Alpha Bound

✓

Let $S \subseteq V$ be a finset, $\alpha \in \mathbb {R}$ with $\alpha {\lt} 1$. If $(|S| : \mathbb {R}) {\lt} \alpha \cdot |V|$, then $|S| {\lt} |V|$ (as natural numbers).

Proof ▶

We show $(|S| : \mathbb {R}) {\lt} |V|$ and then cast to natural numbers. We have:

\[ (|S| : \mathbb {R}) {\lt} \alpha \cdot |V| {\lt} 1 \cdot |V| = |V|, \]

where the second inequality holds because $\alpha {\lt} 1$ and $|V| {\gt} 0$ (the latter follows since $|S| {\lt} \alpha \cdot |V|$ with $\alpha {\gt} 0$ and $|S| \geq 0$ implies $|V| {\gt} 0$; if $|V| = 0$ then the right-hand side $\alpha \cdot 0 = 0$ and $|S| \geq 0$, which combined with $|S| {\lt} 0$ gives a contradiction). Casting back to natural numbers gives $|S| {\lt} |V|$.

Theorem 292 Relative Cheeger Inequality

✓

Let $G = (V, E)$ be a finite, connected, $s$-regular simple graph, and let $\lambda _2$ denote its second-largest adjacency eigenvalue (well-defined since $|V| \geq 2$). Let $\alpha \in (0,1)$ and let $S \subseteq V$ with $0 {\lt} |S|$ and $|S| {\lt} \alpha \cdot |V|$. Then:

\[ (1 - \alpha )(s - \lambda _2) \leq \frac{|\delta S|}{|S|}. \]

Proof ▶

Let $h_{\mathrm{card}} : |V| \geq 2$ be the witness obtained from $|S| {\lt} \alpha \cdot |V|$, $0 {\lt} |S|$, $\alpha {\lt} 1$ via the lemma card_ge_two_of_subset, so that $\lambda _2$ is well-defined.

We establish the following auxiliary facts:

$(|S| : \mathbb {R}) {\gt} 0$ by casting $0 {\lt} |S|$.
$(|V| : \mathbb {R}) {\gt} 0$ since $|V| \geq 2$.
$|S| {\lt} |V|$ (as natural numbers) by card_lt_of_alpha.
$|S|/|V| {\lt} \alpha $ by card_div_lt_alpha.
$1 - \alpha {\lt} 1 - |S|/|V|$ by linear arithmetic from $|S|/|V| {\lt} \alpha $.
$1 - \alpha {\gt} 0$ by linear arithmetic from $\alpha {\lt} 1$.

We invoke the spectral Laplacian bound axiom $(\texttt{spectralLaplacianBound})$ to obtain:

\[ (s - \lambda _2) \cdot |S| \cdot \left(1 - \frac{|S|}{|V|}\right) \leq |\delta S|. \tag {$*$} \]

We also note $|\delta S| \geq 0$ and $1 - |S|/|V| {\gt} 0$ (since $|S| {\lt} |V|$ and $|V| {\gt} 0$).

We now split on the sign of $s - \lambda _2$.

Case 1: $s - \lambda _2 \geq 0$. We multiply out and rewrite the goal $(1 - \alpha )(s - \lambda _2) \leq |\delta S|/|S|$ equivalently (multiplying both sides by $|S| {\gt} 0$) as $(1 - \alpha )(s - \lambda _2) \cdot |S| \leq |\delta S|$. We compute:

\begin{align*} (1 - \alpha )(s - \lambda _2) \cdot |S| & = (s - \lambda _2) \cdot |S| \cdot (1 - \alpha ) \quad \text{(by ring)} \\ & \leq (s - \lambda _2) \cdot |S| \cdot \left(1 - \frac{|S|}{|V|}\right) \quad \text{(since $1 - \alpha \leq 1 - |S|/|V|$ and $(s-\lambda _2)\cdot |S| \geq 0$)} \\ & \leq |\delta S| \quad \text{(by $(*)$)}. \end{align*}

Case 2: $s - \lambda _2 {\lt} 0$. Then $(1-\alpha )(s - \lambda _2) {\lt} 0$ (product of positive $1-\alpha {\gt} 0$ and negative $s - \lambda _2 {\lt} 0$). We have:

\[ (1 - \alpha )(s - \lambda _2) \leq 0 \leq \frac{|\delta S|}{|S|}, \]

where the second inequality holds since $|\delta S| \geq 0$ and $|S| {\gt} 0$.

In both cases the inequality is established.