noncomputable def AlgoLib.nG {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] : ℝ

Equations

• AlgoLib.nG G = ↑G.vertexFinset.card

noncomputable def AlgoLib.xS {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] (S : Finset α) : α → ℝ

Equations

• AlgoLib.xS G S = fun (v : α) => if v ∈ S then AlgoLib.nG G - ↑S.card else -↑S.card

theorem AlgoLib.xS_orth {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] (d : ℕ) (S : Finset α) (hS_nonempty : S.Nonempty) (hS_subset : S ⊆ G.vertexFinset) (h_reg : ∀ v ∈ G.vertexFinset, G.degree v = d) : have x := xS G S; ∑ v ∈ G.vertexFinset, ↑(G.degree v) * x v = 0

theorem AlgoLib.lambda_le_rq {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] (S : Finset α) (hS_nonempty : S.Nonempty) (hS_size : 2 * S.card ≤ G.vertexFinset.card) (hS_subset : S ⊆ G.vertexFinset) (h_orth : ∑ v ∈ G.vertexFinset, ↑(G.degree v) * xS G S v = 0) : have x := xS G S; lambda2 G ≤ G.rayleighQuotient x

noncomputable def AlgoLib.edge_diff_sq {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] (x : α → ℝ) : Sym2 α → ℝ

Equations

• AlgoLib.edge_diff_sq G x = Sym2.lift ⟨fun (u v : α) => (x u - x v) ^ 2, ⋯⟩

theorem AlgoLib.num_eq {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] (S : Finset α) (hS_nonempty : S.Nonempty) : have n := nG G; have x := xS G S; have dS := Cut G S; have edge_diff := edge_diff_sq G x; ∑ e ∈ G.edgeFinset, edge_diff e = n ^ 2 * ↑dS.card

theorem AlgoLib.denom_eq {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] (d : ℕ) (S : Finset α) (hS_size : 2 * S.card ≤ G.vertexFinset.card) (hS_subset : S ⊆ G.vertexFinset) : have n := nG G; have s := ↑S.card; have x := xS G S; ↑d * ∑ v ∈ G.vertexFinset, x v ^ 2 = ↑d * n * s * (n - s)

theorem AlgoLib.rq_eq {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] (d : ℕ) (S : Finset α) (hS_nonempty : S.Nonempty) (hS_size : 2 * S.card ≤ G.vertexFinset.card) (hS_subset : S ⊆ G.vertexFinset) (h_reg : ∀ v ∈ G.vertexFinset, G.degree v = d) : have n := nG G; have s := ↑S.card; have x := xS G S; have dS := Cut G S; have num := n ^ 2 * ↑dS.card; have denom := ↑d * n * s * (n - s); G.rayleighQuotient x = num / denom

theorem AlgoLib.rq_le_two_phi {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] (d : ℕ) (S : Finset α) (hS_nonempty : S.Nonempty) (hS_size : 2 * S.card ≤ G.vertexFinset.card) (hS_subset : S ⊆ G.vertexFinset) (h_reg : ∀ v ∈ G.vertexFinset, G.degree v = d) (hd : d > 0) : have x := xS G S; G.rayleighQuotient x ≤ 2 * edgeExpansion G d S

theorem AlgoLib.cheeger_easy_direction {α : Type u_1} (G : SimpleGraph α) [Fintype ↑G.vertexSet] [DecidableEq α] [DecidablePred fun (x : Sym2 α) => x ∈ G.edgeSet] (d : ℕ) (S : Finset α) (hS_nonempty : S.Nonempty) (hS_size : 2 * S.card ≤ G.vertexFinset.card) (hS_subset : S ⊆ G.vertexFinset) (h_reg : ∀ v ∈ G.vertexFinset, G.degree v = d) (hd : d > 0) : lambda2 G / 2 ≤ edgeExpansion G d S