Isoperimetric problems

References

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

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

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

Equations

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

Isoperimetry and early related results

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

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

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

∂S = E(S, Sᶜ).

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

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

Equations

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

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

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

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

theorem WeightedGraph.Isoperimetry.cheeger_mul_volume_le_volume_frontier {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [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 WeightedGraph.Isoperimetry.connected_iff_cheeger_pos {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] : Connected ↔ 0 < cheeger G

A graph is connected iff its cheeger constant is positive.

theorem WeightedGraph.Isoperimetry.two_cheeger_ge_first_eigval : True

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