Submodularity of directed cut bounds

This file proves that the capacity of the arrows leaving a vertex set is submodular. It then expresses the signed upper cut bound for lower and upper arrow bounds as an outgoing capacity plus a modular vertex-weight function, proving that this more general cut bound is also submodular. These facts let the minimum-cut lattice apply both to ordinary directed networks and to bounded assignments with signed lower bounds.

Main results

• TauCeti.isSubmodular_outgoingArrowSum: nonnegative outgoing arrow capacity is submodular.
• TauCeti.cutBound_eq_arrowSum_sub_sum_excessAt: the upper cut bound is an outgoing arrow sum shifted by the excess of the lower bound.
• TauCeti.isSubmodular_cutBound: a pair of ordered signed bounds has a submodular upper cut bound.

theorem TauCeti.isSubmodular_outgoingArrowSum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(x y : V) → Fintype (Q x y)] [AddCommMonoid K] [Preorder K] [IsOrderedAddMonoid K] (cap : Assignment Q K) (hcap : 0 ≤ cap) : IsSubmodular fun (S : Finset V) => arrowSum cap S Sᶜ

The capacity of arrows leaving a vertex set is submodular when every arrow capacity is nonnegative. Loops, parallel arrows, and arrows in both directions are allowed.

theorem TauCeti.cutBound_eq_arrowSum_sub_sum_excessAt {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] (lo hi : Assignment Q K) (S : Finset V) : cutBound lo hi S = arrowSum (hi - lo) S Sᶜ - ∑ v ∈ S, excessAt lo v

The signed upper cut bound is the outgoing arrow sum for the difference between upper and lower bounds, minus the total excess of the lower bound on the source side.

theorem TauCeti.isSubmodular_cutBound {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [DecidableEq V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] [IsOrderedAddMonoid K] (lo hi : Assignment Q K) (h : lo ≤ hi) : IsSubmodular (cutBound lo hi)

The signed upper cut bound is submodular whenever the lower bound is at most the upper bound. No feasibility assumption on the bounds is needed.