structure MinCut.Multigraph (V : Type u_1) [Fintype V] [DecidableEq V] : Type u_1

• edgeMult : V → V → ℕ
• symm (u v : V) : self.edgeMult u v = self.edgeMult v u
• no_loops (v : V) : self.edgeMult v v = 0

def MinCut.Multigraph.degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (v : V) : ℕ

def MinCut.Multigraph.cutValue {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (S : Finset V) : ℕ

def MinCut.Multigraph.IsMinCut {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (S : Finset V) : Prop

theorem MinCut.Multigraph.cutValue_singleton {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (v : V) : G.cutValue {v} = G.degree v

theorem MinCut.Multigraph.degree_ge_minCut {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (S : Finset V) (hS : G.IsMinCut S) (v : V) (hV : 2 ≤ Fintype.card V) : G.cutValue S ≤ G.degree v

theorem MinCut.Multigraph.sum_degrees_ge_card_mul_minCut {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (S : Finset V) (hS : G.IsMinCut S) (hV : 2 ≤ Fintype.card V) : Fintype.card V * G.cutValue S ≤ ∑ v : V, G.degree v

theorem MinCut.Multigraph.mincut_edge_fraction_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (S : Finset V) (hS : G.IsMinCut S) (hV : 2 ≤ Fintype.card V) (hE : 0 < ∑ v : V, G.degree v) : ↑(G.cutValue S) / ((∑ v : V, ↑(G.degree v)) / 2) ≤ 2 / ↑(Fintype.card V)

theorem MinCut.prod_range_sub_cast_eq_descFactorial (n m : ℕ) (h : m ≤ n) : ∏ i ∈ Finset.range m, (↑n - ↑i) = ↑(n.descFactorial m)

theorem MinCut.contraction_survival_product_eq (n : ℕ) (hn : 2 ≤ n) : ∏ i ∈ Finset.range (n - 2), (↑n - ↑i - 2) / (↑n - ↑i) = 2 / (↑n * (↑n - 1))

theorem MinCut.contraction_survival_product_one_sub (n : ℕ) (hn : 2 ≤ n) : ∏ i ∈ Finset.range (n - 2), (1 - 2 / (↑n - ↑i)) = 2 / (↑n * (↑n - 1))

noncomputable def MinCut.Multigraph.contractionSurvivalProb {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (S : Finset V) : ℝ

theorem MinCut.Multigraph.contractionSurvivalProb_ge_prod {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (S : Finset V) (hS : G.IsMinCut S) (hV : 2 ≤ Fintype.card V) : G.contractionSurvivalProb S ≥ ∏ i ∈ Finset.range (Fintype.card V - 2), (1 - 2 / (↑(Fintype.card V) - ↑i))

theorem MinCut.contraction_algorithm_success_prob {V : Type u_1} [Fintype V] [DecidableEq V] (G : Multigraph V) (S : Finset V) (hS : G.IsMinCut S) (hV : 2 ≤ Fintype.card V) : G.contractionSurvivalProb S ≥ 2 / (↑(Fintype.card V) * (↑(Fintype.card V) - 1))