Lemma 3: Relative Vertex-to-Edge Expansion

Main Results

• relativeVertexToEdgeExpansion: For a finite, connected, s-regular graph with second-largest eigenvalue λ₂, parameter α ∈ (0,1), subset S with |S| ≤ α|V|, and 0 < b ≤ s, define A = {v ∈ S | |(δS)_v| ≥ s - b} and β = ((b - λ₂) - α(s - λ₂))/b. Then |A| ≥ β|S|.

Definitions

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

The edges in the edge boundary δS incident to vertex v (for SimpleGraph).

Equations

• RelativeVertexToEdgeExpansion.edgeBoundaryAtVertex G S v = {e ∈ CheegerConstant.edgeBoundary G S | v ∈ e}

noncomputable def RelativeVertexToEdgeExpansion.highExpansionVertices {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (s : ℕ) (b : ℝ) : Finset V

The set A = {v ∈ S | |(δS)_v| ≥ s - b}: vertices in S with high boundary degree.

Equations

• RelativeVertexToEdgeExpansion.highExpansionVertices G S s b = {v ∈ S | ↑s - b ≤ ↑(RelativeVertexToEdgeExpansion.edgeBoundaryAtVertex G S v).card}

theorem RelativeVertexToEdgeExpansion.highExpansionVertices_subset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (s : ℕ) (b : ℝ) : highExpansionVertices G S s b ⊆ S

A ⊆ S.

theorem RelativeVertexToEdgeExpansion.highExpansionVertices_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (s : ℕ) (b : ℝ) (h : ∃ v ∈ S, ↑s - b ≤ ↑(edgeBoundaryAtVertex G S v).card) : (highExpansionVertices G S s b).Nonempty

Witness: highExpansionVertices is nonempty when there exists a vertex in S with high boundary degree.

Partition of the edge boundary

Each edge in δS has exactly one endpoint in S, so {(δS)_v}_{v ∈ S} partitions δS. This gives |δS| = ∑_{v ∈ S} |(δS)_v|.

theorem RelativeVertexToEdgeExpansion.edgeBoundary_partition_sum {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : (CheegerConstant.edgeBoundary G S).card = ∑ v ∈ S, (edgeBoundaryAtVertex G S v).card

The edge boundary card equals the sum of edgeBoundaryAtVertex cards over S.

Degree bound

theorem RelativeVertexToEdgeExpansion.edgeBoundaryAtVertex_le_degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) (S : Finset V) (v : V) : (edgeBoundaryAtVertex G S v).card ≤ s

The number of boundary edges incident to v is at most s (the degree).

Helper: Relative Cheeger with ≤

theorem RelativeVertexToEdgeExpansion.relativeCheeger_le {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_le : ↑S.card ≤ α * ↑(Fintype.card V)) (hcard : 2 ≤ Fintype.card V) : (1 - α) * (↑s - GraphExpansion.secondLargestEigenvalue G hcard) * ↑S.card ≤ ↑(CheegerConstant.edgeBoundary G S).card

The relative Cheeger bound with |S| ≤ α|V| (non-strict). Derived from the spectralLaplacianBound axiom in Lem_1.

Step 2: Upper bound on |δS|

theorem RelativeVertexToEdgeExpansion.edgeBoundary_upper_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (b : ℝ) (hreg : G.IsRegularOfDegree s) (S : Finset V) : have A := highExpansionVertices G S s b; ↑(CheegerConstant.edgeBoundary G S).card ≤ ↑s * ↑A.card + (↑s - b) * (↑S.card - ↑A.card)

The upper bound |δS| ≤ s|A| + (s-b)|B| where B = S \ A.

Main Theorem

theorem RelativeVertexToEdgeExpansion.relativeVertexToEdgeExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (α b : ℝ) (hα0 : 0 < α) (hα1 : α < 1) (hb0 : 0 < b) (hbs : b ≤ ↑s) (hconn : G.Connected) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) (S : Finset V) (hS_le : ↑S.card ≤ α * ↑(Fintype.card V)) : have lam2 := GraphExpansion.secondLargestEigenvalue G hcard; have A := highExpansionVertices G S s b; (b - lam2 - α * (↑s - lam2)) / b * ↑S.card ≤ ↑A.card

Relative Vertex-to-Edge Expansion. For a finite, connected, s-regular graph with second-largest eigenvalue λ₂, α ∈ (0,1), S ⊆ V with |S| ≤ α|V|, and 0 < b ≤ s, define A = {v ∈ S | |(δS)_v| ≥ s - b} and β = ((b - λ₂) - α(s - λ₂))/b. Then |A| ≥ β|S|.