24 Def 18: Cheeger Constant
Let \(G = (V, E)\) be a finite simple graph with a decidable adjacency relation, and let \(S \subseteq V\) be a finite subset of vertices. The edge boundary \(\delta S\) is the finite set of edges in \(G\) that cross the cut determined by \(S\):
Formally, using the quotient representation \(\operatorname {Sym2}(V)\) for unordered pairs, we set
Let \(G\) be a finite simple graph with decidable adjacency, \(S \subseteq V\) a finite subset, and \(e \in \operatorname {Sym2}(V)\). Then
We prove both directions.
\((\Rightarrow )\): Assume \(e \in \delta S\). By the definition of \(\delta S\) (filtering \(G.\operatorname {edgeFinset}\)), we obtain \(e \in E(G)\) and the disjunction \((e.\operatorname {out}_1 \in S \land e.\operatorname {out}_2 \notin S) \lor (e.\operatorname {out}_2 \in S \land e.\operatorname {out}_1 \notin S)\). In the first case, set \(a = e.\operatorname {out}_1\) and \(b = e.\operatorname {out}_2\); then \(\{ a, b\} = e\) by the identity \(e = \operatorname {Sym2.mk}(e.\operatorname {out})\), and \(a \in S\), \(b \notin S\). In the second case, set \(a = e.\operatorname {out}_2\) and \(b = e.\operatorname {out}_1\); then \(\{ a, b\} = \{ b, a\} = e\) by symmetry of \(\operatorname {Sym2}\), and again \(a \in S\), \(b \notin S\).
\((\Leftarrow )\): Assume \(e \in E(G)\) and there exist \(a \in S\), \(b \notin S\) with \(\{ a, b\} = e\). We substitute \(e = \{ a, b\} \). Let \((p, q) = \{ a, b\} .\operatorname {out}\); by the characterization \(\operatorname {Sym2.mk_eq_mk_iff}\), either \((p, q) = (a, b)\) or \((p, q) = (b, a)\). In the first sub-case, \(p = a \in S\) and \(q = b \notin S\), giving the left disjunct. In the second sub-case, \(p = b\) and \(q = a\), so \(q = a \in S\) and \(p = b \notin S\), giving the right disjunct. Hence \(e \in \delta S\).
For any finite simple graph \(G\) with decidable adjacency and any \(S \subseteq V\), the edge boundary satisfies \(\delta S \subseteq E(G)\).
This follows immediately from the fact that \(\delta S\) is defined as a filter of \(G.\operatorname {edgeFinset}\), and any filter of a finset is a subset of it: \(\operatorname {Finset.filter_subset}\).
Let \(G\) be a finite simple graph, \(S \subseteq V\) a finite subset, and \(u, v \in V\) with \(G.\operatorname {Adj}(u, v)\). If \(u \in S\) and \(v \notin S\), then \(\{ u, v\} \in \delta S\).
We rewrite using the membership characterization of the edge boundary (Theorem 278). It suffices to provide \(\{ u, v\} \in E(G)\) (which holds since \(G.\operatorname {Adj}(u, v)\) implies \(\{ u, v\} \in G.\operatorname {edgeFinset}\)) and the witnesses \(a = u \in S\), \(b = v \notin S\) with \(\{ u, v\} = \{ u, v\} \) (by reflexivity).
A finite subset \(S \subseteq V\) is called eligible (for the Cheeger constant) if:
\(S\) is nonempty: \(S \neq \emptyset \), and
\(S\) is at most half the vertex set: \(2|S| \leq |V|\).
Formally, \(\operatorname {EligibleSubset}(S) \; \Longleftrightarrow \; S.\operatorname {Nonempty} \land 2 \cdot |S| \leq |V|\).
Let \(G\) be a finite simple graph with decidable adjacency, and let \(S \subseteq V\) be a finite subset. The isoperimetric ratio of \(S\) is
where \(|\delta S|\) denotes the cardinality of the edge boundary and \(|S|\) the cardinality of \(S\).
Let \(G\) be a finite simple graph with decidable adjacency. The Cheeger constant (or isoperimetric number) of \(G\) is
where the infimum is taken over all eligible subsets \(S\) (nonempty subsets with \(2|S| \leq |V|\)). When no eligible subset exists (i.e., \(|V| {\lt} 2\)), the set is empty and \(h(G) = 0\) by the convention \(\operatorname {sInf}\, \emptyset = 0\) for \(\mathbb {R}\).
If \(|V| \geq 2\), then there exists an eligible subset \(S \subseteq V\).
Since \(|V| \geq 2 {\gt} 0\), the type \(V\) is nonempty. Obtain a vertex \(v \in V\). Consider the singleton \(S = \{ v\} \). Then \(S\) is nonempty by \(\operatorname {Finset.singleton_nonempty}\), and \(|S| = 1\), so \(2 \cdot |S| = 2 \leq |V|\) by hypothesis. By integer arithmetic (\(\omega \)), the condition \(2 \cdot 1 \leq |V|\) follows from \(|V| \geq 2\). Hence \(\{ v\} \) is an eligible subset.
For any finite simple graph \(G\) with decidable adjacency, \(h(G) \geq 0\).
We unfold the definition of \(h(G)\) and consider two cases.
Case 1: \(|V| \geq 2\). By Theorem 284, obtain an eligible subset \(S\). The set \(\bigl\{ \, r \; \big|\; \exists \, S',\; \operatorname {EligibleSubset}(S') \land h(S') = r\, \bigr\} \) is nonempty (witnessed by \(h(S)\)). We apply \(\operatorname {le_csInf}\): it suffices to show every element \(r = h(S')\) in the set satisfies \(0 \leq r\). But \(r = |\delta S'| / |S'|\), which is nonneg by positivity (both numerator and denominator are nonneg naturals cast to \(\mathbb {R}\)).
Case 2: \(|V| {\lt} 2\). Since \(|V| {\lt} 2\), any eligible subset \(S\) would require \(S\) nonempty (\(|S| \geq 1\)) and \(2|S| \leq |V| {\lt} 2\), giving \(|S| {\lt} 1\), a contradiction. Hence no eligible subset exists, the defining set is empty, and \(h(G) = \operatorname {sInf}\, \emptyset = 0 \geq 0\) by the real conditionally complete lattice convention.
red[UNPROVEN AXIOM]
Let \(G\) be a connected \(s\)-regular finite simple graph on vertex set \(V\) with \(|V| \geq 2\). Let \(\lambda _2 = \lambda _2(G)\) denote the second-largest adjacency eigenvalue of \(G\) (Definition 242), and let \(h(G)\) be the Cheeger constant of \(G\) (Definition 283). Then the following Cheeger inequalities hold:
The lower bound follows from the variational characterization of \(\lambda _2\) via the Courant–Fischer min-max theorem, and the upper bound follows from a sweep-cut argument applied to the second eigenvector.
Note: This is stated as an axiom because the proof requires spectral theory infrastructure (the Courant–Fischer min-max theorem and sweep-cut analysis) that is not available in Mathlib.