The weight matrix of a multigraph given by its ends

A multigraph given by its ends ends : E → Sym2 V (Cslib.Multigraph) has a weight matrix Cslib.Multigraph.weightMatrix ends counting the edges between distinct vertices; self-loops are dropped. It is a weighted multigraph in the sense of Cslib.WeightedCut.IsMultigraph, and the weight of each cut is the number of edges between the cut and its complement, so the global minimum cut weight of the matrix is the least size of an edge cut of a non-trivial cut.

Main definitions

• Cslib.Multigraph.weightMatrix: the number of edges joining two distinct vertices.

Main results

• Cslib.Multigraph.isMultigraph_weightMatrix: the weight matrix is symmetric with zero diagonal.
• Cslib.Multigraph.cutWeight_weightMatrix: the weight of a cut is the size of its edge cut.
• Cslib.Multigraph.minCut_weightMatrix_le_card_edgeCut: the global minimum cut weight is at most the size of the edge cut of any non-trivial cut.

def Cslib.Multigraph.weightMatrix {V : Type u_1} {E : Type u_2} [Fintype E] [DecidableEq V] (ends : E → Sym2 V) (u v : V) : ℕ

The weight matrix of the multigraph ends: the number of edges joining u and v when they are distinct, and 0 on the diagonal, so self-loops are dropped.

theorem Cslib.Multigraph.isMultigraph_weightMatrix {V : Type u_1} {E : Type u_2} [Fintype E] [DecidableEq V] (ends : E → Sym2 V) : WeightedCut.IsMultigraph (weightMatrix ends)

The weight matrix of a multigraph is symmetric with zero diagonal.

theorem Cslib.Multigraph.cutWeight_weightMatrix {V : Type u_1} {E : Type u_2} [Fintype E] [DecidableEq V] (ends : E → Sym2 V) [Fintype V] (S : Finset V) : WeightedCut.cutWeight (weightMatrix ends) S = (edgeCut ends S).card

The weight of a cut in the weight matrix of a multigraph is the number of edges between the cut and its complement.

theorem Cslib.Multigraph.minCut_weightMatrix_le_card_edgeCut {V : Type u_1} {E : Type u_2} [Fintype E] [DecidableEq V] (ends : E → Sym2 V) [Fintype V] {S : Finset V} (hS : WeightedCut.IsNonTrivialCut S) : WeightedCut.minCut (weightMatrix ends) ≤ (edgeCut ends S).card

The global minimum cut weight of the weight matrix of a multigraph is at most the number of edges leaving any non-trivial cut.

theorem Cslib.Multigraph.exists_card_edgeCut_eq_minCut_weightMatrix {V : Type u_1} {E : Type u_2} [Fintype E] [DecidableEq V] (ends : E → Sym2 V) [Fintype V] (hV : 2 ≤ Fintype.card V) : ∃ (S : Finset V), WeightedCut.IsNonTrivialCut S ∧ (edgeCut ends S).card = WeightedCut.minCut (weightMatrix ends)

With at least two vertices, the global minimum cut weight of the weight matrix of a multigraph is the number of edges leaving some non-trivial cut.