Cheeger Constant (Isoperimetric Number / Edge Expansion)

Statement

For a graph $G = (V, E)$, the Cheeger constant (also called isoperimetric number or edge expansion) is defined as $h(G) = \min_{S \subseteq V, 0 < |S| \leq |V|/2} \frac{|\partial S|}{|S|}$, where $\partial S$ is the edge boundary of $S$, i.e., the set of edges with exactly one endpoint in $S$. A graph is called an expander if $h(G) \geq c$ for some constant $c > 0$. In this work, we require $h(G) \geq 1$ to ensure that the deformed code preserves the distance of the original code.

Main Results

• edgeBoundary: The edge boundary ∂S of a vertex set S
• CheegerConstant: The Cheeger constant h(G)
• IsExpander: Predicate for expander graphs (∃ c > 0, h(G) ≥ c)
• IsStrongExpander: Predicate for h(G) ≥ 1 (used in this work)

Edge Boundary

def QEC1.edgeCrossesBoundary {V : Type u_1} [DecidableEq V] (S : Finset V) (e : Sym2 V) : Bool

Whether an edge crosses the boundary of S (exactly one endpoint in S)

Equations

• QEC1.edgeCrossesBoundary S e = Sym2.lift ⟨fun (u v : V) => decide (u ∈ S ∧ v ∉ S ∨ u ∉ S ∧ v ∈ S), ⋯⟩ e

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

The edge boundary ∂S of a vertex set S is the set of edges with exactly one endpoint in S.

Equations

• QEC1.edgeBoundary G S = {e ∈ G.edgeFinset | QEC1.edgeCrossesBoundary S e = true}

@[simp]

theorem QEC1.mem_edgeBoundary {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (u v : V) : s(u, v) ∈ edgeBoundary G S ↔ G.Adj u v ∧ (u ∈ S ∧ v ∉ S ∨ u ∉ S ∧ v ∈ S)

Cheeger Constant

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

The Cheeger constant h(G) = min_{S : 0 < |S| ≤ |V|/2} |∂S|/|S|. Returns the infimum over all valid subsets.

Equations

• QEC1.CheegerConstant G = ⨅ (S : Finset V), ⨅ (_ : S.Nonempty), ⨅ (_ : 2 * S.card ≤ Fintype.card V), ↑(QEC1.edgeBoundary G S).card / ↑S.card

Expander Graphs

def QEC1.IsExpander {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Prop

A graph is an expander if h(G) ≥ c for some constant c > 0.

Equations

• QEC1.IsExpander G = ∃ c > 0, QEC1.CheegerConstant G ≥ c

def QEC1.IsStrongExpander {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Prop

A strong expander has Cheeger constant at least 1: h(G) ≥ 1. This is the condition required in this work to preserve the distance of the original code.

Equations

• QEC1.IsStrongExpander G = (QEC1.CheegerConstant G ≥ 1)

Basic Properties

@[simp]

theorem QEC1.edgeBoundary_empty {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : edgeBoundary G ∅ = ∅

The edge boundary of the empty set is empty

@[simp]

theorem QEC1.edgeBoundary_univ {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : edgeBoundary G Finset.univ = ∅

The edge boundary of the full vertex set is empty

theorem QEC1.edgeBoundary_compl {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : edgeBoundary G S = edgeBoundary G Sᶜ

The edge boundary is symmetric: ∂S = ∂(V \ S)

theorem QEC1.IsStrongExpander.isExpander {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (h : IsStrongExpander G) : IsExpander G

A strong expander is an expander (with c = 1)

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

Cheeger constant is nonnegative