Cuts of weighted multigraphs

An undirected weighted multigraph without self-loops on a finite vertex type V is given here by its symmetric weight matrix W : V → V → ℕ with zero diagonal (Cslib.WeightedCut.IsMultigraph): W u v is the total weight, or the number of parallel edges, joining distinct u and v. A set C of vertices with C and its complement both nonempty is a non-trivial cut, its weight is the total weight of the edges between C and its complement, and the global minimum cut weight is the least weight of a non-trivial cut.

Contracting a multigraph along a surjective map part : V → U of the vertices onto supervertices sums the weights between the vertices sent to distinct supervertices (Cslib.WeightedCut.IsContractionOf). Pulling a cut of the contracted multigraph back to the original vertices gives a cut of the same weight (Cslib.WeightedCut.cutWeight_pullbackCut), so contraction never decreases the global minimum cut weight. Karger's contraction algorithm and the Karger–Stein algorithm (CslibFrontier.Algorithms.Karger.Graph) are built on these facts.

The multigraphs given by their ends (Cslib.Multigraph) have weight matrices with the same cut weights; see CslibFrontier.Foundations.Combinatorics.WeightedCut.Multigraph.

Main definitions

• Cslib.WeightedCut.IsMultigraph: a symmetric weight matrix with zero diagonal.
• Cslib.WeightedCut.IsNonTrivialCut: a set of vertices whose complement is also nonempty.
• Cslib.WeightedCut.cutWeight, Cslib.WeightedCut.minCut: cut weights and the global minimum cut weight.
• Cslib.WeightedCut.rowDeg, Cslib.WeightedCut.totalDoubledWeight: weighted degrees and their sum, twice the total edge weight.
• Cslib.WeightedCut.pullbackCut, Cslib.WeightedCut.IsContractionOf: cuts pulled back along a supervertex map, and contracted multigraphs.

Main results

• Cslib.WeightedCut.cutWeight_compl: a cut and its complement have the same weight.
• Cslib.WeightedCut.cutWeight_singleton: a singleton cut weighs the degree of its vertex.
• Cslib.WeightedCut.cutWeight_fin_two, Cslib.WeightedCut.totalDoubledWeight_fin_two: on two vertices, every non-trivial cut weighs the weight of the edge, and the degrees sum to twice it.
• Cslib.WeightedCut.le_minCut_iff: with at least two vertices, m ≤ minCut W exactly when every non-trivial cut weighs at least m.
• Cslib.WeightedCut.mul_minCut_le_totalDoubledWeight: |V| * minCut W is at most the sum of the degrees.
• Cslib.WeightedCut.cutWeight_pullbackCut: pulling a cut back along a contraction preserves its weight.
• Cslib.WeightedCut.minCut_le_of_isContractionOf: contraction does not decrease the global minimum cut weight.
• Cslib.WeightedCut.two_vertex_contraction_output: a contraction to two supervertices gives a non-trivial cut of the original multigraph whose weight is the remaining edge weight.

Weighted multigraphs and global minimum cuts

def Cslib.WeightedCut.IsMultigraph {V : Type u_1} (W : V → V → ℕ) : Prop

An undirected weighted multigraph without self-loops on the vertices V is a symmetric weight matrix W : V → V → ℕ with zero diagonal.

def Cslib.WeightedCut.IsNonTrivialCut {V : Type u_1} [Fintype V] (C : Finset V) : Prop

A vertex subset C defines a non-trivial cut when both C and its complement are nonempty.

theorem Cslib.WeightedCut.isNonTrivialCut_iff_card {V : Type u_1} [Fintype V] (C : Finset V) : IsNonTrivialCut C ↔ 0 < C.card ∧ C.card < Fintype.card V

theorem Cslib.WeightedCut.isNonTrivialCut_singleton {V : Type u_1} [Fintype V] (hV : 2 ≤ Fintype.card V) (a : V) : IsNonTrivialCut {a}

theorem Cslib.WeightedCut.exists_isNonTrivialCut {V : Type u_1} [Fintype V] (hV : 2 ≤ Fintype.card V) : ∃ (C : Finset V), IsNonTrivialCut C

def Cslib.WeightedCut.rowDeg {V : Type u_1} [Fintype V] (W : V → V → ℕ) (u : V) : ℕ

Weighted degree of vertex u in W.

def Cslib.WeightedCut.totalDoubledWeight {V : Type u_1} [Fintype V] (W : V → V → ℕ) : ℕ

Sum of all row degrees ∑ u, ∑ v, W u v, equal to twice the total edge weight of W.

theorem Cslib.WeightedCut.entry_le_rowDeg {V : Type u_1} [Fintype V] (W : V → V → ℕ) (u v : V) : W u v ≤ rowDeg W u

theorem Cslib.WeightedCut.rowDeg_le_totalDoubledWeight {V : Type u_1} [Fintype V] (W : V → V → ℕ) (u : V) : rowDeg W u ≤ totalDoubledWeight W

theorem Cslib.WeightedCut.entry_le_totalDoubledWeight {V : Type u_1} [Fintype V] (W : V → V → ℕ) (u v : V) : W u v ≤ totalDoubledWeight W

theorem Cslib.WeightedCut.isNonTrivialCut_compl {V : Type u_1} [Fintype V] [DecidableEq V] {C : Finset V} (hC : IsNonTrivialCut C) : IsNonTrivialCut (Finset.univ \ C)

def Cslib.WeightedCut.cutWeight {V : Type u_1} [Fintype V] [DecidableEq V] {M : Type u_3} [AddCommMonoid M] (W : V → V → M) (C : Finset V) : M

Total weight of edges crossing (C, Finset.univ \ C), for weights in any additive commutative monoid (natural numbers for multigraphs, or a linearly ordered field such as ℝ).

theorem Cslib.WeightedCut.cutWeight_univ_sdiff_of_symm {V : Type u_1} [Fintype V] [DecidableEq V] {M : Type u_3} [AddCommMonoid M] {W : V → V → M} (hW : ∀ (u v : V), W u v = W v u) (C : Finset V) : cutWeight W (Finset.univ \ C) = cutWeight W C

For symmetric weights, the cut (Finset.univ \ C, C) weighs as much as (C, Finset.univ \ C).

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

theorem Cslib.WeightedCut.cutWeight_le_sum_rowDeg {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) (C : Finset V) : cutWeight W C ≤ ∑ u ∈ C, rowDeg W u

theorem Cslib.WeightedCut.two_mul_cutWeight_le_totalDoubledWeight {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} (hW : IsMultigraph W) (C : Finset V) : 2 * cutWeight W C ≤ totalDoubledWeight W

theorem Cslib.WeightedCut.cutWeight_singleton {V : Type u_1} [Fintype V] [DecidableEq V] {W : V → V → ℕ} (hW : IsMultigraph W) (a : V) : cutWeight W {a} = rowDeg W a

theorem Cslib.WeightedCut.cutWeight_two_singleton_zero {W : Fin 2 → Fin 2 → ℕ} (hW : IsMultigraph W) : cutWeight W {0} = W 0 1

theorem Cslib.WeightedCut.cutWeight_fin_two {W : Fin 2 → Fin 2 → ℕ} (hW : IsMultigraph W) {B : Finset (Fin 2)} (hB : IsNonTrivialCut B) : cutWeight W B = W 0 1

On two vertices, every non-trivial cut weighs the weight of the edge.

theorem Cslib.WeightedCut.totalDoubledWeight_fin_two {W : Fin 2 → Fin 2 → ℕ} (hW : IsMultigraph W) : totalDoubledWeight W = 2 * W 0 1

On two vertices, the sum of the degrees is twice the weight of the edge.

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

Global minimum cut weight of a multigraph W, defined as the greatest lower bound of cutWeight W C over all non-trivial cuts C.

theorem Cslib.WeightedCut.minCut_le_cutWeight {V : Type u_1} [Fintype V] [DecidableEq V] (W : V → V → ℕ) {C : Finset V} (hC : IsNonTrivialCut C) : minCut W ≤ cutWeight W C

theorem Cslib.WeightedCut.exists_minCut_achiever {V : Type u_1} [Fintype V] [DecidableEq V] (hV : 2 ≤ Fintype.card V) (W : V → V → ℕ) : ∃ (C : Finset V), IsNonTrivialCut C ∧ cutWeight W C = minCut W

theorem Cslib.WeightedCut.le_minCut_iff {V : Type u_1} [Fintype V] [DecidableEq V] (hV : 2 ≤ Fintype.card V) (W : V → V → ℕ) (m : ℕ) : m ≤ minCut W ↔ ∀ (C : Finset V), IsNonTrivialCut C → m ≤ cutWeight W C

theorem Cslib.WeightedCut.minCut_pos_iff {V : Type u_1} [Fintype V] [DecidableEq V] (hV : 2 ≤ Fintype.card V) (W : V → V → ℕ) : 0 < minCut W ↔ ∀ (C : Finset V), IsNonTrivialCut C → 0 < cutWeight W C

theorem Cslib.WeightedCut.minCut_le_rowDeg {V : Type u_1} [Fintype V] [DecidableEq V] (hV : 2 ≤ Fintype.card V) {W : V → V → ℕ} (hW : IsMultigraph W) (a : V) : minCut W ≤ rowDeg W a

theorem Cslib.WeightedCut.mul_minCut_le_totalDoubledWeight {V : Type u_1} [Fintype V] [DecidableEq V] (hV : 2 ≤ Fintype.card V) {W : V → V → ℕ} (hW : IsMultigraph W) : Fintype.card V * minCut W ≤ totalDoubledWeight W

theorem Cslib.WeightedCut.totalDoubledWeight_pos_of_minCut_pos {V : Type u_1} [Fintype V] [DecidableEq V] (hV : 2 ≤ Fintype.card V) {W : V → V → ℕ} (hW : IsMultigraph W) (hpos : 0 < minCut W) : 0 < totalDoubledWeight W

Supervertex maps and contractions

def Cslib.WeightedCut.pullbackCut {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] (part : V → U) (B : Finset U) : Finset V

Pull back a cut B of the supervertices along a supervertex map part : V → U.

theorem Cslib.WeightedCut.mem_pullbackCut {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] (part : V → U) (B : Finset U) (x : V) : x ∈ pullbackCut part B ↔ part x ∈ B

theorem Cslib.WeightedCut.pullbackCut_empty {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] (part : V → U) : pullbackCut part ∅ = ∅

structure Cslib.WeightedCut.IsContractionOf {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] (W₀ : V → V → ℕ) (part : V → U) (W : U → U → ℕ) : Prop

W : U → U → ℕ is the contracted multigraph of W₀ : V → V → ℕ along the surjective supervertex assignment part : V → U: the weight between distinct supervertices is the total weight between the vertices sent to them.

• surj : Function.Surjective part
• multigraph : IsMultigraph W
• offDiag (a b : U) : a ≠ b → W a b = ∑ x : V with part x = a, ∑ y : V with part y = b, W₀ x y

theorem Cslib.WeightedCut.pullbackCut_univ {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] [Fintype U] (part : V → U) : pullbackCut part Finset.univ = Finset.univ

theorem Cslib.WeightedCut.isNonTrivialCut_pullbackCut {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] [Fintype U] {part : V → U} (hsurj : Function.Surjective part) {B : Finset U} (hB : IsNonTrivialCut B) : IsNonTrivialCut (pullbackCut part B)

theorem Cslib.WeightedCut.isNonTrivialCut_of_pullbackCut {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] [Fintype U] (part : V → U) {B : Finset U} (h : IsNonTrivialCut (pullbackCut part B)) : IsNonTrivialCut B

theorem Cslib.WeightedCut.pullbackCut_compl {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] [Fintype U] [DecidableEq V] (part : V → U) (B : Finset U) : pullbackCut part (Finset.univ \ B) = Finset.univ \ pullbackCut part B

theorem Cslib.WeightedCut.isContractionOf_id {V : Type u_1} [Fintype V] [DecidableEq V] {W₀ : V → V → ℕ} (hW₀ : IsMultigraph W₀) : IsContractionOf W₀ id W₀

theorem Cslib.WeightedCut.cutWeight_pullbackCut {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] [Fintype U] [DecidableEq V] {W₀ : V → V → ℕ} {part : V → U} {W : U → U → ℕ} (hC : IsContractionOf W₀ part W) (B : Finset U) : cutWeight W₀ (pullbackCut part B) = cutWeight W B

theorem Cslib.WeightedCut.minCut_le_of_isContractionOf {V : Type u_1} {U : Type u_2} [Fintype V] [DecidableEq U] [Fintype U] [DecidableEq V] (hU : 2 ≤ Fintype.card U) {W₀ : V → V → ℕ} {part : V → U} {W : U → U → ℕ} (hC : IsContractionOf W₀ part W) : minCut W₀ ≤ minCut W

theorem Cslib.WeightedCut.two_vertex_contraction_output {V : Type u_1} [Fintype V] [DecidableEq V] {W₀ : V → V → ℕ} {part : V → Fin 2} {W : Fin 2 → Fin 2 → ℕ} (hC : IsContractionOf W₀ part W) : IsNonTrivialCut (pullbackCut part {0}) ∧ W 0 1 = cutWeight W₀ (pullbackCut part {0}) ∧ minCut W₀ ≤ W 0 1