Minimum cuts between two vertices of a weighted multigraph

For a weighted multigraph W : V → V → ℕ (Cslib.WeightedCut.IsMultigraph) and vertices s and t, the minimum s–t cut weight λ(s, t) = Cslib.WeightedCut.minCutBetween W s t is the least weight cutWeight W X of a vertex set X containing s and missing t (and 0 when s = t). By max-flow min-cut it is the value of a maximum s–t flow; see CslibFrontier.Algorithms.Lean.GomoryHu.WeightedCut.

The cut function X ↦ cutWeight W X is submodular, and posimodular for a multigraph (symmetric W). The values λ satisfy the ultrametric triangle inequality λ(u, w) ≥ min (λ(u, v)) (λ(v, w)), the basic fact behind Gomory–Hu trees ([GH61]; [Sch03], Section 15.4).

Main definitions

• Cslib.WeightedCut.minCutBetween: the minimum s–t cut weight λ(s, t).

Main results

• Cslib.WeightedCut.exists_cutWeight_eq_minCutBetween: for s ≠ t, some set containing s and missing t has weight λ(s, t).
• Cslib.WeightedCut.le_minCutBetween_iff: for s ≠ t, m ≤ λ(s, t) exactly when every set containing s and missing t weighs at least m.
• Cslib.WeightedCut.minCutBetween_comm: λ(s, t) = λ(t, s) for a multigraph.
• Cslib.WeightedCut.cutWeight_union_add_cutWeight_inter_le_of_nonneg: submodularity of the cut function of non-negative weights in an ordered additive monoid (ℕ, ℝ, ...), and its ℕ case Cslib.WeightedCut.cutWeight_union_add_cutWeight_inter_le.
• Cslib.WeightedCut.cutWeight_sdiff_add_cutWeight_sdiff_le_of_symm: posimodularity of the cut function of symmetric non-negative weights, and its multigraph case Cslib.WeightedCut.cutWeight_sdiff_add_cutWeight_sdiff_le.
• Cslib.WeightedCut.min_le_minCutBetween: the triangle inequality min (λ(u, v)) (λ(v, w)) ≤ λ(u, w).

References

• [GH61]
• [Sch03]

theorem Cslib.WeightedCut.cutWeight_compl_of_symm {V : Type u_1} [Fintype V] [DecidableEq V] {M : Type u_2} [AddCommMonoid M] {W : V → V → M} (hW : ∀ (u v : V), W u v = W v u) (X : Finset V) : cutWeight W Xᶜ = cutWeight W X

For symmetric weights, the complement Xᶜ of a cut weighs as much as X.

theorem Cslib.WeightedCut.cutWeight_union_add_cutWeight_inter_le_of_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] (W : V → V → M) (hW : ∀ (u v : V), 0 ≤ W u v) (A B : Finset V) : cutWeight W (A ∪ B) + cutWeight W (A ∩ B) ≤ cutWeight W A + cutWeight W B

The cut function of non-negative weights is submodular: w(δ(A ∪ B)) + w(δ(A ∩ B)) ≤ w(δ(A)) + w(δ(B)). Symmetry of W is not needed.

theorem Cslib.WeightedCut.cutWeight_sdiff_add_cutWeight_sdiff_le_of_symm {V : Type u_1} [Fintype V] [DecidableEq V] {M : Type u_2} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {W : V → V → M} (hWs : ∀ (u v : V), W u v = W v u) (hWn : ∀ (u v : V), 0 ≤ W u v) (A B : Finset V) : cutWeight W (A \ B) + cutWeight W (B \ A) ≤ cutWeight W A + cutWeight W B

The cut function of symmetric non-negative weights is posimodular: w(δ(A \ B)) + w(δ(B \ A)) ≤ w(δ(A)) + w(δ(B)).

theorem Cslib.WeightedCut.cutWeight_compl' {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} (hW : IsMultigraph W) (X : Finset V) : cutWeight W Xᶜ = cutWeight W X

The weight of the complement Xᶜ of a cut of a multigraph is the weight of X.

theorem Cslib.WeightedCut.cutWeight_union_add_cutWeight_inter_le {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) (A B : Finset V) : cutWeight W (A ∪ B) + cutWeight W (A ∩ B) ≤ cutWeight W A + cutWeight W B

The cut function is submodular: w(δ(A ∪ B)) + w(δ(A ∩ B)) ≤ w(δ(A)) + w(δ(B)). Symmetry of W is not needed.

theorem Cslib.WeightedCut.cutWeight_sdiff_add_cutWeight_sdiff_le {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} (hW : IsMultigraph W) (A B : Finset V) : cutWeight W (A \ B) + cutWeight W (B \ A) ≤ cutWeight W A + cutWeight W B

The cut function of a multigraph is posimodular: w(δ(A \ B)) + w(δ(B \ A)) ≤ w(δ(A)) + w(δ(B)).

noncomputable def Cslib.WeightedCut.minCutBetween {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) (s t : V) : ℕ

The minimum s–t cut weight λ(s, t) of a weighted multigraph W: the least weight of a vertex set containing s and missing t, and 0 when s = t.

theorem Cslib.WeightedCut.minCutBetween_le_cutWeight {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) {s t : V} {X : Finset V} (hs : s ∈ X) (ht : t ∉ X) : minCutBetween W s t ≤ cutWeight W X

@[simp]

theorem Cslib.WeightedCut.minCutBetween_self {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) (s : V) : minCutBetween W s s = 0

theorem Cslib.WeightedCut.exists_cutWeight_eq_minCutBetween {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) {s t : V} (hst : s ≠ t) : ∃ (X : Finset V), s ∈ X ∧ t ∉ X ∧ cutWeight W X = minCutBetween W s t

For distinct s and t, the minimum s–t cut weight is attained.

theorem Cslib.WeightedCut.le_minCutBetween_iff {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) {s t : V} (hst : s ≠ t) (m : ℕ) : m ≤ minCutBetween W s t ↔ ∀ (X : Finset V), s ∈ X → t ∉ X → m ≤ cutWeight W X

theorem Cslib.WeightedCut.cutWeight_eq_minCutBetween_iff {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) {s t : V} {X : Finset V} (hs : s ∈ X) (ht : t ∉ X) : cutWeight W X = minCutBetween W s t ↔ ∀ (Y : Finset V), s ∈ Y → t ∉ Y → cutWeight W X ≤ cutWeight W Y

A set containing s and missing t is a minimum s–t cut exactly when its weight is at most that of every such set.

theorem Cslib.WeightedCut.minCutBetween_comm {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} (hW : IsMultigraph W) (s t : V) : minCutBetween W s t = minCutBetween W t s

The minimum cut weight between two vertices of a multigraph is symmetric.

theorem Cslib.WeightedCut.min_le_minCutBetween {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) {u w : V} (huw : u ≠ w) (v : V) : min (minCutBetween W u v) (minCutBetween W v w) ≤ minCutBetween W u w

Triangle inequality for minimum cuts ([GH61]): for distinct u and w and any v, min (λ(u, v)) (λ(v, w)) ≤ λ(u, w). A minimum u–w cut separates v from u or from w. Symmetry of W is not needed.

theorem Cslib.WeightedCut.minCutBetween_eq_of_lt {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} (hW : IsMultigraph W) {u v w : V} (huv : u ≠ v) (h : minCutBetween W u v < minCutBetween W v w) : minCutBetween W u w = minCutBetween W u v

Among the three values λ(u, v), λ(v, w), λ(u, w) of a multigraph, the minimum is attained at least twice: if λ(u, v) < λ(v, w) then λ(u, w) = λ(u, v).