Flows between vertex sets

Let Q be an arrow family on a finite vertex type V with capacities cap, and let A and B be finite vertex sets. An A–B flow is an arrow assignment between zero and the capacities that is conserved at every vertex outside A ∪ B, has nonpositive excess at every vertex of A and nonnegative excess at every vertex of B. Its value is its total excess on B, which is minus its total excess on A. An A–B cut is a vertex set containing A and avoiding B, an admissible side in the sense of TauCeti.TerminalCut.IsAdmissible, and its capacity is the total capacity of the arrows leaving it. Either set may be empty, in which case every A–B flow has value zero.

For disjoint A and B this file proves the max-flow/min-cut theorem between vertex sets: weak duality, the augmenting-path optimality criterion, the existence of an A–B flow and an A–B cut of equal value and capacity, and integrality in an additive subgroup containing the capacities. Here an augmenting walk runs from a vertex of A to a vertex of B along residual arrows of positive capacity.

The existence results come from the reduction to single terminals. Add a fresh source with an arrow to each a ∈ A of capacity the total capacity leaving a, and a fresh sink with an arrow from each b ∈ B of capacity the total capacity entering b (TauCeti.setFlowCapacity). The A–B flows then correspond exactly to the ordinary flows between the fresh terminals, with the same values on the original arrows and the same value (TauCeti.SetFlow.auxFlowEquiv), and normalizing a minimum cut between the fresh terminals gives a minimum A–B cut of the same capacity (TauCeti.TerminalCut.IsMinimum.isMinimum_union_sdiff, in TauCeti.Combinatorics.Network.AuxiliaryTerminals).

Main definitions

• TauCeti.SetFlow cap A B: A–B flows for the capacities cap, with value SetFlow.val.
• TauCeti.SetFlow.IsMaximum: an A–B flow of largest value.
• TauCeti.SetFlow.toAuxFlow and TauCeti.Flow.toSetFlow: the ordinary flow of the auxiliary network corresponding to an A–B flow, and the A–B flow corresponding to an ordinary flow of the auxiliary network.
• TauCeti.SetFlow.auxFlowEquiv: the correspondence between A–B flows and ordinary flows of the auxiliary network.

Main results

• TauCeti.SetFlow.val_eq_arrowSum_sub: the value is the net value across every A–B cut.
• TauCeti.SetFlow.val_le_arrowSum: weak duality.
• TauCeti.SetFlow.tfae_isMaximum: an A–B flow is maximum exactly when it has no augmenting walk, and exactly when its value is the capacity of some A–B cut.
• TauCeti.TerminalCut.isAdmissible_filter_positiveReachable: without augmenting walks, the vertices positively reachable from A form an A–B cut.
• TauCeti.SetFlow.exists_isMaximum_mem: integrality of maximum A–B flows.
• TauCeti.SetFlow.exists_val_eq_arrowSum: the max-flow/min-cut theorem between vertex sets.

References

• L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 10.

structure TauCeti.SetFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] (cap : Assignment Q K) (A B : Finset V) : Type (max (max u v) w)

An A–B flow for the capacities cap: an arrow assignment between zero and cap that is conserved at every vertex outside A ∪ B, with nonpositive excess at every vertex of A and nonnegative excess at every vertex of B.

• toFun : Assignment Q K

  The value on each arrow.

• mem_Icc : self.toFun ∈ Set.Icc 0 cap

  The assignment lies between zero and the capacities.

• conserve (v : V) : v ∉ A → v ∉ B → excessAt self.toFun v = 0

  The assignment is conserved at every vertex outside A ∪ B.

• excessAt_nonpos (a : V) : a ∈ A → excessAt self.toFun a ≤ 0

  Every vertex of A is a supply vertex.

• excessAt_nonneg (b : V) : b ∈ B → 0 ≤ excessAt self.toFun b

  Every vertex of B is a demand vertex.

theorem TauCeti.SetFlow.ext {V : Type u} {Q : V → V → Type v} {K : Type w} {inst✝ : Fintype V} {inst✝¹ : (v w : V) → Fintype (Q v w)} {inst✝² : AddCommGroup K} {inst✝³ : Preorder K} {cap : Assignment Q K} {A B : Finset V} {x y : SetFlow cap A B} (toFun : x.toFun = y.toFun) : x = y

theorem TauCeti.SetFlow.ext_iff {V : Type u} {Q : V → V → Type v} {K : Type w} {inst✝ : Fintype V} {inst✝¹ : (v w : V) → Fintype (Q v w)} {inst✝² : AddCommGroup K} {inst✝³ : Preorder K} {cap : Assignment Q K} {A B : Finset V} {x y : SetFlow cap A B} : x = y ↔ x.toFun = y.toFun

theorem TauCeti.TerminalCut.isAdmissible_filter_positiveReachable {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [Zero K] [LT K] {c : Assignment Q K} {A B : Finset V} (h : ∀ a ∈ A, ∀ b ∈ B, ¬PositiveReachable c a b) : IsAdmissible A B {v : V | ∃ a ∈ A, PositiveReachable c a v}

If no vertex of B is positively reachable from a vertex of A for the capacities c, then the vertices positively reachable from A form an A–B cut.

theorem TauCeti.SetFlow.nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {cap : Assignment Q K} {A B : Finset V} (f : SetFlow cap A B) {x y : V} (e : Q x y) : 0 ≤ f.toFun e

theorem TauCeti.SetFlow.le_cap {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {cap : Assignment Q K} {A B : Finset V} (f : SetFlow cap A B) {x y : V} (e : Q x y) : f.toFun e ≤ cap e

def TauCeti.SetFlow.val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {cap : Assignment Q K} {A B : Finset V} (f : SetFlow cap A B) : K

The value of an A–B flow: its total excess on B.

theorem TauCeti.SetFlow.val_def {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {cap : Assignment Q K} {A B : Finset V} (f : SetFlow cap A B) : f.val = ∑ b ∈ B, excessAt f.toFun b

def TauCeti.SetFlow.IsMaximum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {cap : Assignment Q K} {A B : Finset V} (f : SetFlow cap A B) : Prop

An A–B flow is maximum when it maximizes the value among all A–B flows for the same capacities.

theorem TauCeti.SetFlow.isMaximum_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {cap : Assignment Q K} {A B : Finset V} {f : SetFlow cap A B} : f.IsMaximum ↔ ∀ (g : SetFlow cap A B), g.val ≤ f.val

theorem TauCeti.SetFlow.excessAt_eq_zero_of_mem_of_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} (f : SetFlow cap A B) {v : V} (hA : v ∈ A) (hB : v ∈ B) : excessAt f.toFun v = 0

An A–B flow is conserved at every vertex of A ∩ B.

theorem TauCeti.SetFlow.sum_excessAt_source {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} (f : SetFlow cap A B) : ∑ a ∈ A, excessAt f.toFun a = -f.val

The total excess of an A–B flow on A is minus its value.

@[simp]

theorem TauCeti.SetFlow.val_empty_right {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A : Finset V} (f : SetFlow cap A ∅) : f.val = 0

An A–B flow with no demand vertices has value zero.

@[simp]

theorem TauCeti.SetFlow.val_empty_left {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {B : Finset V} (f : SetFlow cap ∅ B) : f.val = 0

An A–B flow with no supply vertices has value zero.

theorem TauCeti.SetFlow.val_eq_arrowSum_sub {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [DecidableEq V] (f : SetFlow cap A B) {S : Finset V} (hS : TerminalCut.IsAdmissible A B S) : f.val = arrowSum f.toFun S Sᶜ - arrowSum f.toFun Sᶜ S

The value of an A–B flow is the value on arrows leaving S minus the value on arrows entering S, for every A–B cut S.

theorem TauCeti.SetFlow.arrowSum_sub_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [DecidableEq V] (f : SetFlow cap A B) {S : Finset V} (hS : TerminalCut.IsAdmissible A B S) : arrowSum cap S Sᶜ - f.val = arrowSum (residualCapacity 0 cap f.toFun) S Sᶜ

Residual cut gap. For every A–B cut S, the capacity of S exceeds the value of an A–B flow by its total residual capacity on the residual arrows leaving S.

theorem TauCeti.SetFlow.val_nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (f : SetFlow cap A B) : 0 ≤ f.val

The value of an A–B flow is nonnegative.

theorem TauCeti.SetFlow.val_le_arrowSum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] [DecidableEq V] (f : SetFlow cap A B) {S : Finset V} (hS : TerminalCut.IsAdmissible A B S) : f.val ≤ arrowSum cap S Sᶜ

Weak duality. The value of an A–B flow is at most the capacity of every A–B cut.

theorem TauCeti.SetFlow.val_eq_arrowSum_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] [DecidableEq V] (f : SetFlow cap A B) {S : Finset V} (hS : TerminalCut.IsAdmissible A B S) : f.val = arrowSum cap S Sᶜ ↔ ∀ v ∈ S, ∀ w ∉ S, ∀ (e : ResidualHom Q v w), residualCapacity 0 cap f.toFun e = 0

An A–B flow attains the capacity of an A–B cut S exactly when every residual arrow leaving S has zero residual capacity.

theorem TauCeti.SetFlow.isMaximum_of_val_eq_arrowSum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] [DecidableEq V] (f : SetFlow cap A B) {S : Finset V} (hS : TerminalCut.IsAdmissible A B S) (h : f.val = arrowSum cap S Sᶜ) : f.IsMaximum

An A–B flow whose value is the capacity of an A–B cut is maximum.

theorem TauCeti.SetFlow.val_eq_arrowSum_of_not_positiveReachable {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] [DecidableEq V] (f : SetFlow cap A B) (h : ∀ a ∈ A, ∀ b ∈ B, ¬PositiveReachable (residualCapacity 0 cap f.toFun) a b) : f.val = arrowSum cap {v : V | ∃ a ∈ A, PositiveReachable (residualCapacity 0 cap f.toFun) a v} {v : V | ∃ a ∈ A, PositiveReachable (residualCapacity 0 cap f.toFun) a v}ᶜ

If no vertex of B is positively reachable from a vertex of A for the residual capacities of an A–B flow, then its value is the capacity of the set of vertices positively reachable from A, which is an A–B cut.

theorem TauCeti.SetFlow.exists_val_lt_of_positiveReachable {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {A B : Finset V} (hAB : Disjoint A B) (f : SetFlow cap A B) {a b : V} (ha : a ∈ A) (hb : b ∈ B) (h : PositiveReachable (residualCapacity 0 cap f.toFun) a b) : ∃ (g : SetFlow cap A B), f.val < g.val

Augmentation. If a vertex of B is positively reachable from a vertex of A for the residual capacities of an A–B flow, for disjoint A and B, then augmenting along an augmenting path by its bottleneck gives an A–B flow of larger value.

theorem TauCeti.SetFlow.IsMaximum.not_positiveReachable {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {A B : Finset V} (hAB : Disjoint A B) {f : SetFlow cap A B} (hf : f.IsMaximum) {a b : V} (ha : a ∈ A) (hb : b ∈ B) : ¬PositiveReachable (residualCapacity 0 cap f.toFun) a b

A maximum A–B flow for disjoint A and B has no augmenting walk.

theorem TauCeti.SetFlow.tfae_isMaximum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {A B : Finset V} [DecidableEq V] (hAB : Disjoint A B) (f : SetFlow cap A B) : [f.IsMaximum, ∀ a ∈ A, ∀ b ∈ B, ¬PositiveReachable (residualCapacity 0 cap f.toFun) a b, ∃ (S : Finset V), TerminalCut.IsAdmissible A B S ∧ f.val = arrowSum cap S Sᶜ].TFAE

Augmenting-path optimality criterion for A–B flows. For an A–B flow f between disjoint vertex sets, the following are equivalent: f is maximum; there is no augmenting walk for f from a vertex of A to a vertex of B; and the value of f equals the capacity of some A–B cut.

theorem TauCeti.SetFlow.IsMaximum.exists_val_eq_arrowSum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {A B : Finset V} [DecidableEq V] (hAB : Disjoint A B) {f : SetFlow cap A B} (hf : f.IsMaximum) : ∃ (S : Finset V), TerminalCut.IsAdmissible A B S ∧ f.val = arrowSum cap S Sᶜ

A maximum A–B flow between disjoint vertex sets saturates some A–B cut.

theorem TauCeti.SetFlow.excessAt_auxTerminalCapacity_inl {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} (f : SetFlow cap A B) (v : V) : excessAt (auxTerminalCapacity f.toFun (fun (a : V) => -excessAt f.toFun a) fun (b : V) => excessAt f.toFun b) (Sum.inl v) = 0

The assignment of the auxiliary network corresponding to an A–B flow is conserved at every original vertex.

theorem TauCeti.SetFlow.auxTerminalCapacity_le_setFlowCapacity {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (f : SetFlow cap A B) : (auxTerminalCapacity f.toFun (fun (a : V) => -excessAt f.toFun a) fun (b : V) => excessAt f.toFun b) ≤ setFlowCapacity cap A B

The assignment of the auxiliary network corresponding to an A–B flow lies below the auxiliary capacities setFlowCapacity cap A B.

def TauCeti.SetFlow.toAuxFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (f : SetFlow cap A B) : Flow (setFlowCapacity cap A B) (Sum.inr false) (Sum.inr true)

The ordinary flow from the fresh source to the fresh sink of the auxiliary network corresponding to an A–B flow. It keeps the values on the original arrows, and carries minus the excess at a on the arrow from the fresh source to a ∈ A and the excess at b on the arrow from b ∈ B to the fresh sink.

@[simp]

theorem TauCeti.SetFlow.toAuxFlow_toFun {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (f : SetFlow cap A B) : f.toAuxFlow.toFun = auxTerminalCapacity f.toFun (fun (a : V) => -excessAt f.toFun a) fun (b : V) => excessAt f.toFun b

def TauCeti.Flow.toSetFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (g : Flow (setFlowCapacity cap A B) (Sum.inr false) (Sum.inr true)) (hAB : Disjoint A B) : SetFlow cap A B

The A–B flow corresponding to an ordinary flow from the fresh source to the fresh sink of the auxiliary network, for disjoint A and B: its restriction to the original arrows.

@[simp]

theorem TauCeti.Flow.toSetFlow_toFun {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (g : Flow (setFlowCapacity cap A B) (Sum.inr false) (Sum.inr true)) (hAB : Disjoint A B) : (g.toSetFlow hAB).toFun = auxTerminalRestrict g.toFun

def TauCeti.SetFlow.auxFlowEquiv {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (hAB : Disjoint A B) : SetFlow cap A B ≃ Flow (setFlowCapacity cap A B) (Sum.inr false) (Sum.inr true)

Reduction to single terminals. For disjoint A and B, the A–B flows correspond to the ordinary flows from the fresh source to the fresh sink for the auxiliary capacities setFlowCapacity cap A B, by SetFlow.toAuxFlow and Flow.toSetFlow. An A–B flow keeps its values on the original arrows, and carries minus its excess at a on the arrow from the fresh source to a ∈ A and its excess at b on the arrow from b ∈ B to the fresh sink.

@[simp]

theorem TauCeti.SetFlow.auxFlowEquiv_apply {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (hAB : Disjoint A B) (f : SetFlow cap A B) : (auxFlowEquiv hAB) f = f.toAuxFlow

@[simp]

theorem TauCeti.SetFlow.auxFlowEquiv_symm_apply {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (hAB : Disjoint A B) (g : Flow (setFlowCapacity cap A B) (Sum.inr false) (Sum.inr true)) : (auxFlowEquiv hAB).symm g = g.toSetFlow hAB

@[simp]

theorem TauCeti.SetFlow.toAuxFlow_toSetFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (hAB : Disjoint A B) (f : SetFlow cap A B) : f.toAuxFlow.toSetFlow hAB = f

@[simp]

theorem TauCeti.SetFlow.val_toAuxFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (f : SetFlow cap A B) : f.toAuxFlow.val = f.val

The ordinary flow of the auxiliary network corresponding to an A–B flow has the same value.

@[simp]

theorem TauCeti.Flow.toSetFlow_toAuxFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (hAB : Disjoint A B) (g : Flow (setFlowCapacity cap A B) (Sum.inr false) (Sum.inr true)) : (g.toSetFlow hAB).toAuxFlow = g

@[simp]

theorem TauCeti.Flow.val_toSetFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (hAB : Disjoint A B) (g : Flow (setFlowCapacity cap A B) (Sum.inr false) (Sum.inr true)) : (g.toSetFlow hAB).val = g.val

The A–B flow corresponding to an ordinary flow of the auxiliary network has the same value.

@[simp]

theorem TauCeti.SetFlow.isMaximum_toAuxFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [PartialOrder K] {cap : Assignment Q K} {A B : Finset V} [IsOrderedAddMonoid K] (hAB : Disjoint A B) {f : SetFlow cap A B} : f.toAuxFlow.IsMaximum ↔ f.IsMaximum

An A–B flow is maximum exactly when the corresponding flow of the auxiliary network is.

theorem TauCeti.SetFlow.exists_isMaximum_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {A B : Finset V} (hAB : Disjoint A B) (hcap : 0 ≤ cap) (H : AddSubgroup K) (hcapH : ∀ ⦃v w : V⦄ (e : Q v w), cap e ∈ H) : ∃ (f : SetFlow cap A B), f.IsMaximum ∧ ∀ ⦃v w : V⦄ (e : Q v w), f.toFun e ∈ H

Integrality of maximum A–B flows. For disjoint A and B and nonnegative capacities in an additive subgroup H, some maximum A–B flow takes values in H.

theorem TauCeti.SetFlow.exists_isMaximum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {A B : Finset V} (hAB : Disjoint A B) (hcap : 0 ≤ cap) : ∃ (f : SetFlow cap A B), f.IsMaximum

For disjoint A and B and nonnegative capacities, a maximum A–B flow exists.

theorem TauCeti.SetFlow.exists_val_eq_arrowSum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] [LinearOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {A B : Finset V} (hAB : Disjoint A B) (hcap : 0 ≤ cap) : ∃ (f : SetFlow cap A B) (S : Finset V), TerminalCut.IsAdmissible A B S ∧ f.val = arrowSum cap S Sᶜ

Max-flow/min-cut theorem between vertex sets. For disjoint A and B and nonnegative capacities, some A–B flow has value equal to the capacity of some A–B cut. By weak duality (TauCeti.SetFlow.val_le_arrowSum) this flow is maximum and this cut is minimum.

Example

On the vertices 0, 1, 2, 3, take unit capacities on the arrows 0 → 2, 0 → 3 and 1 → 3, and capacity zero on one arrow for every other ordered pair, loops included. For the supply vertices A = {0, 1} and the demand vertices B = {2, 3}, the assignment saturating every arrow is an A–B flow with excesses -2, -1, 1, 2, so of value 3. This is the capacity of the cut A, so the flow is maximum. The corresponding flow of the auxiliary network also has value 3, and carries 2 on the arrow from the fresh source to 0.

For the same vertex and arrow types, take unit capacities in both directions between 0 and 1 and zero capacities elsewhere. Saturating these two arrows is a nonzero circulation. With no supply vertices and demand vertices {2, 3}, it is a set flow of value zero. Its corresponding auxiliary flow retains the unit value on the original arrow 0 → 1 and also has value zero.