Capacities of undirected cuts

This file defines the capacity of a cut in a weighted multigraph. Parallel edges contribute separately and loops never contribute. Aggregating the weights of all edges with the same unordered pair of distinct ends therefore preserves every cut capacity.

For a simple graph, the multigraph cut capacity of Graph.ofSimpleGraph G agrees with TauCeti.pairCutCapacity when pair capacities vanish away from the edges of G.

Main definitions

• Graph.edgeCutCapacity: the capacity of a cut in a weighted multigraph.
• Graph.pairCapacity: aggregation of multigraph edge weights by their distinct ends.
• SimpleGraph.ofSimpleGraphCapacity: restriction of pair capacities to actual edges.

Main result

• Graph.edgeCutCapacity_one: a unit-capacity cut has value equal to the number of crossing edge identities.
• Graph.pairCutCapacity_pairCapacity: aggregation preserves every cut capacity.
• Graph.isSubmodular_edgeCutCapacity: an edge-capacity function nonnegative on nonloop edges has a submodular cut function.
• Graph.isSymmSubmodular_edgeCutCapacity: the bundled symmetric-submodular result.
• SimpleGraph.edgeCutCapacity_eq_pairCutCapacity: the simple-graph and multigraph cut-capacity interfaces agree.

noncomputable def Graph.edgeCutCapacity {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.edgeSet] [AddCommMonoid K] (c : ↑G.edgeSet → K) (S : Finset ↑G.vertexSet) : K

The capacity of a cut in a weighted multigraph. Each actual crossing edge is counted once.

theorem Graph.edgeCutCapacity_def {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.edgeSet] [AddCommMonoid K] (c : ↑G.edgeSet → K) (S : Finset ↑G.vertexSet) [DecidablePred fun (e : ↑G.edgeSet) => ↑e ∈ G.edgeCut (Subtype.val '' ↑S)] : G.edgeCutCapacity c S = ∑ e : ↑G.edgeSet, if ↑e ∈ G.edgeCut (Subtype.val '' ↑S) then c e else 0

The defining finite-sum formula for edgeCutCapacity.

@[simp]

theorem Graph.edgeCutCapacity_one {V : Type u_1} {E : Type u_2} (G : Graph V E) [Fintype ↑G.edgeSet] (S : Finset ↑G.vertexSet) : G.edgeCutCapacity (fun (x : ↑G.edgeSet) => 1) S = (G.edgeCut (Subtype.val '' ↑S)).ncard

Giving every actual edge capacity one makes the capacity of a cut equal to the number of crossing edge identities. In particular, parallel edges are counted separately.

noncomputable def Graph.pairCapacity {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.edgeSet] [AddCommMonoid K] (c : ↑G.edgeSet → K) (p : Sym2 ↑G.vertexSet) : K

Aggregate edge weights by the unordered pair of their distinct ends. The capacity of every diagonal pair is zero, so loops are discarded.

theorem Graph.pairCapacity_def {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.edgeSet] [AddCommMonoid K] (c : ↑G.edgeSet → K) (p : Sym2 ↑G.vertexSet) [DecidablePred fun (e : ↑G.edgeSet) => ¬p.IsDiag ∧ G.edgeEnds e = p] : G.pairCapacity c p = ∑ e : ↑G.edgeSet, if ¬p.IsDiag ∧ G.edgeEnds e = p then c e else 0

The defining finite-sum formula for pairCapacity.

theorem Graph.pairCapacity_mk_of_ne {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.edgeSet] [AddCommMonoid K] (c : ↑G.edgeSet → K) {x y : ↑G.vertexSet} (hxy : x ≠ y) [DecidablePred fun (e : ↑G.edgeSet) => G.IsLink ↑e ↑x ↑y] : G.pairCapacity c s(x, y) = ∑ e : ↑G.edgeSet, if G.IsLink ↑e ↑x ↑y then c e else 0

On a pair of distinct vertices, pairCapacity sums exactly the weights of edges linking those vertices.

@[simp]

theorem Graph.pairCapacity_mk_self {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.edgeSet] [AddCommMonoid K] (c : ↑G.edgeSet → K) (x : ↑G.vertexSet) : G.pairCapacity c s(x, x) = 0

Aggregated pair capacity vanishes on a diagonal pair.

theorem Graph.pairCapacity_eq_zero_of_isDiag {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.edgeSet] [AddCommMonoid K] (c : ↑G.edgeSet → K) {p : Sym2 ↑G.vertexSet} (hp : p.IsDiag) : G.pairCapacity c p = 0

Aggregated pair capacity vanishes on diagonal pairs, independently of loop weights.

theorem Graph.pairCutCapacity_pairCapacity {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet] [AddCommMonoid K] (c : ↑G.edgeSet → K) (S : Finset ↑G.vertexSet) : TauCeti.pairCutCapacity (G.pairCapacity c) S = G.edgeCutCapacity c S

Aggregating parallel edge weights by their distinct ends preserves every cut capacity.

@[simp]

theorem Graph.edgeCutCapacity_compl {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet] [DecidableEq ↑G.vertexSet] [AddCommMonoid K] (c : ↑G.edgeSet → K) (S : Finset ↑G.vertexSet) : G.edgeCutCapacity c Sᶜ = G.edgeCutCapacity c S

Multigraph cut capacity is unchanged when the two sides of the cut are exchanged.

theorem Graph.isSubmodular_edgeCutCapacity {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.edgeSet] [DecidableEq ↑G.vertexSet] [AddCommMonoid K] [Preorder K] [IsOrderedAddMonoid K] (c : ↑G.edgeSet → K) (hc : ∀ (e : ↑G.edgeSet), ¬(G.edgeEnds e).IsDiag → 0 ≤ c e) : TauCeti.IsSubmodular (G.edgeCutCapacity c)

The cut function of edge weights nonnegative on nonloop edges is submodular. Together with edgeCutCapacity_compl, this makes it a symmetric submodular set function. Parallel edges are counted separately, and loop weights are unrestricted.

theorem Graph.isSymmSubmodular_edgeCutCapacity {V : Type u_1} {E : Type u_2} {K : Type u_3} (G : Graph V E) [Fintype ↑G.vertexSet] [Fintype ↑G.edgeSet] [DecidableEq ↑G.vertexSet] [AddCommMonoid K] [Preorder K] [IsOrderedAddMonoid K] (c : ↑G.edgeSet → K) (hc : ∀ (e : ↑G.edgeSet), ¬(G.edgeEnds e).IsDiag → 0 ≤ c e) : TauCeti.IsSymmSubmodular (G.edgeCutCapacity c)

The cut function of edge weights nonnegative on nonloop edges is symmetric submodular. Loop weights are unrestricted.

@[instance_reducible]

noncomputable instance SimpleGraph.instFintypeOfSimpleGraphVertexSet {V : Type u_1} (G : SimpleGraph V) [Fintype V] : Fintype ↑(Graph.ofSimpleGraph G).vertexSet

The vertex set of the multigraph realization of a finite simple graph is finite.

@[instance_reducible]

noncomputable instance SimpleGraph.instFintypeOfSimpleGraphEdgeSet {V : Type u_1} (G : SimpleGraph V) [Fintype V] : Fintype ↑(Graph.ofSimpleGraph G).edgeSet

The edge set of the multigraph realization of a finite simple graph is finite.

def SimpleGraph.ofSimpleGraphCapacity {V : Type u_1} {K : Type u_2} (G : SimpleGraph V) (c : Sym2 V → K) : ↑(Graph.ofSimpleGraph G).edgeSet → K

Restrict capacities on unordered vertex pairs to the actual edges of Graph.ofSimpleGraph G.

@[simp]

theorem SimpleGraph.ofSimpleGraphCapacity_apply {V : Type u_1} {K : Type u_2} (G : SimpleGraph V) (c : Sym2 V → K) (e : ↑(Graph.ofSimpleGraph G).edgeSet) : G.ofSimpleGraphCapacity c e = c ↑e

def SimpleGraph.toOfSimpleGraphVertex {V : Type u_1} (G : SimpleGraph V) (x : V) : ↑(Graph.ofSimpleGraph G).vertexSet

Include a vertex of a simple graph in the full vertex set of Graph.ofSimpleGraph G.

@[simp]

theorem SimpleGraph.toOfSimpleGraphVertex_val {V : Type u_1} (G : SimpleGraph V) (x : V) : ↑(G.toOfSimpleGraphVertex x) = x

def SimpleGraph.toOfSimpleGraphFinset {V : Type u_1} (G : SimpleGraph V) (S : Finset V) : Finset ↑(Graph.ofSimpleGraph G).vertexSet

Include a finite vertex set in the full vertex set of Graph.ofSimpleGraph G.

@[simp]

theorem SimpleGraph.mem_toOfSimpleGraphFinset {V : Type u_1} (G : SimpleGraph V) {S : Finset V} {x : V} : G.toOfSimpleGraphVertex x ∈ G.toOfSimpleGraphFinset S ↔ x ∈ S

@[simp]

theorem SimpleGraph.image_val_toOfSimpleGraphFinset {V : Type u_1} (G : SimpleGraph V) (S : Finset V) : Subtype.val '' ↑(G.toOfSimpleGraphFinset S) = ↑S

@[simp]

theorem SimpleGraph.toOfSimpleGraphFinset_map_val {V : Type u_1} (G : SimpleGraph V) (S : Finset ↑(Graph.ofSimpleGraph G).vertexSet) : G.toOfSimpleGraphFinset (Finset.map { toFun := Subtype.val, inj' := ⋯ } S) = S

theorem SimpleGraph.edgeCutCapacity_eq_pairCutCapacity {V : Type u_1} {K : Type u_2} (G : SimpleGraph V) [Fintype V] [AddCommMonoid K] (c : Sym2 V → K) (hc : ∀ (p : Sym2 V), ¬p.IsDiag → p ∉ G.edgeSet → c p = 0) (S : Finset V) : (Graph.ofSimpleGraph G).edgeCutCapacity (G.ofSimpleGraphCapacity c) (G.toOfSimpleGraphFinset S) = TauCeti.pairCutCapacity c S

The multigraph cut capacity of Graph.ofSimpleGraph G agrees with pair cut capacity when capacities vanish away from the edges of G.