Isoperimetric problems

References

• [Spectral Graph Theory, Fan Chung][Chung]

def UnweightedGraph.edgeConnection {α : Type u_1} {β : Type u_2} {G : UnweightedGraph α β} (A B : Set α) : Set β

E(A, B) denotes the set of edges with one endpoint in A and one endpoint in B.

Equations

• UnweightedGraph.edgeConnection A B = {e : β | e ∈ G.edgeSet ∧ ∃ a ∈ A, ∃ b ∈ B, G.IsLink e a b}

Isoperimetry and early related results

theorem UnweightedGraph.Isoperimetry.edgeBoundaryComplement {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] (S : Set α) : edgeBoundary S = edgeBoundary Sᶜ

It is easy to see that ∂S = ∂Sᶜ.

theorem UnweightedGraph.Isoperimetry.self_connection_eq_boundary {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] (S : Set α) : edgeBoundary S = edgeConnection S Sᶜ

∂S = E(S, Sᶜ).

noncomputable def UnweightedGraph.Isoperimetry.hG {α : Type u_1} {β : Type u_2} [Fintype α] {G : UnweightedGraph α β} (S : Set α) : ℝ

For a vertex set S, we define hG(S) = |E(S, Sᶜ)| / min(vol S , vol Sᶜ).

Equations

• UnweightedGraph.Isoperimetry.hG S = ↑(UnweightedGraph.edgeBoundary S).ncard / ↑(min (UnweightedGraph.vol S) (UnweightedGraph.vol Sᶜ))

noncomputable def UnweightedGraph.Isoperimetry.gG {α : Type u_1} {β : Type u_2} [Fintype α] {G : UnweightedGraph α β} (S : Set α) : ℝ

For a vertex set S, we define its vertex expansion as gG(S) = |vol δS| / min(vol S , vol Sᶜ).

Equations

• UnweightedGraph.Isoperimetry.gG S = ↑(UnweightedGraph.vol (UnweightedGraph.vertexBoundary S)) / ↑(min (UnweightedGraph.vol S) (UnweightedGraph.vol Sᶜ))

noncomputable def UnweightedGraph.Isoperimetry.cheeger {α : Type u_1} {β : Type u_2} [Fintype α] (G : UnweightedGraph α β) : ℝ

The Cheeger constant of a graph G is defined as the minimum of hG (S) for every set of vertices S with non-zero volume and co-volume.

Equations

• UnweightedGraph.Isoperimetry.cheeger G = ⨅ (S : Set α), ⨅ (_ : 0 < min (UnweightedGraph.vol S) (UnweightedGraph.vol Sᶜ)), UnweightedGraph.Isoperimetry.hG S

noncomputable def UnweightedGraph.Isoperimetry.cheegerV {α : Type u_1} {β : Type u_2} [Fintype α] (G : UnweightedGraph α β) : ℝ

The Vertex Cheeger constant of a graph G is defined as the minimum of gG (S) for every set of vertices S with non-zero volume and co-volume.

Equations

• UnweightedGraph.Isoperimetry.cheegerV G = ⨅ (S : Set α), ⨅ (_ : 0 < min (UnweightedGraph.vol S) (UnweightedGraph.vol Sᶜ)), UnweightedGraph.Isoperimetry.gG S

theorem UnweightedGraph.Isoperimetry.cheeger_mul_volume_le_volume_frontier {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] (S : Set α) (hc : 0 < min (vol S) (vol Sᶜ)) (hPb1 : vol S ≤ vol Sᶜ) : cheeger G * ↑(vol S) ≤ ↑(edgeBoundary S).ncard

cheger * vol S ≤ |∂S|.

theorem UnweightedGraph.Isoperimetry.connected_iff_cheeger_pos {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] : Connected ↔ 0 < cheeger G

A graph is connected iff its cheeger constant is positive.

theorem UnweightedGraph.Isoperimetry.two_cheeger_ge_eigval_1 {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] [OfNat (Fin (Fintype.card α)) 0] [OfNat (Fin (Fintype.card α)) 1] : lapEigvals 1 ≤ 2 * cheeger G

We first derive a simple upper bound for the eigenvalue λ₁ in terms of the Cheeger constant of a connected graph.

theorem UnweightedGraph.Isoperimetry.cheeger_lower_bound : True

For a connected graph G, λ₁ > hG²/2.

theorem UnweightedGraph.Isoperimetry.hG_le_gG {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] [OfNat (Fin (Fintype.card α)) 0] [OfNat (Fin (Fintype.card α)) 1] (S : Set α) : hG S ≤ gG S

theorem UnweightedGraph.Isoperimetry.cheeger_le_cheegerV {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] [OfNat (Fin (Fintype.card α)) 0] [OfNat (Fin (Fintype.card α)) 1] : cheeger G ≤ cheegerV G

theorem UnweightedGraph.Isoperimetry.two_cheegerV_ge_first_eigval : True