noncomputable def CanonicalPaths.edgesCut {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : ℕ

noncomputable def CanonicalPaths.volume {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : ℕ

noncomputable def CanonicalPaths.conductanceSet {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : ℝ

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

noncomputable def CanonicalPaths.maxDegree {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ

def CanonicalPaths.CanonicalPathSystem {V : Type u_1} (G : SimpleGraph V) : Type u_1

noncomputable def CanonicalPaths.congestion {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (paths : CanonicalPathSystem G) (e : Sym2 V) : ℕ

theorem CanonicalPaths.walk_crosses_cut {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) {u v : V} (hu : u ∈ S) (hv : v ∉ S) (p : G.Walk u v) : ∃ e ∈ p.edges, ∃ (a : V) (b : V), e = s(a, b) ∧ a ∈ S ∧ b ∉ S

theorem CanonicalPaths.conductance_lower_bound {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (paths : CanonicalPathSystem G) (b : ℝ) (hb : 0 < b) (hdmax : 0 < ↑(maxDegree G)) (hV : 0 < Fintype.card V) (hcong : ∀ e ∈ G.edgeFinset, ↑(congestion G paths e) ≤ b * ↑(Fintype.card V)) : conductance G ≥ 1 / (4 * b * ↑(maxDegree G))