Bounded terminal assignments, flows, and weak duality

Let Q be an arrow family on a finite vertex type V with lower and upper bounds lo hi : Assignment Q K. A bounded s–t assignment is an arrow assignment between the bounds that is conserved at every vertex other than the terminals s and t; its value is its excess at t, of either sign. An ordinary s–t flow for capacities cap is the special case with zero lower bounds and nonnegative value. Both share the arrow assignments, excess calculus and residual updates of TauCeti.Combinatorics.Network.Excess and TauCeti.Combinatorics.Network.Residual.

The value of a bounded s–t assignment is the net value across every vertex set S containing s but not t. This gives weak duality: the value is at most the cut bound hi(δ⁺ S) - lo(δ⁻ S), and for an ordinary flow at most the capacity cap(δ⁺ S) of the cut. A residual s–t assignment within the residual capacities updates a bounded s–t assignment to another one, adding the two values, and every bounded s–t assignment arises from any other in this way. These are the steps from which the augmenting-path characterization of maximum flows is assembled.

Main definitions

• TauCeti.BoundedFlow lo hi s t: bounded s–t assignments, with value BoundedFlow.val.
• TauCeti.cutBound lo hi S: the total upper bound leaving S minus the total lower bound entering S.
• TauCeti.BoundedFlow.swap: the same assignment as a bounded t–s assignment.
• TauCeti.BoundedFlow.update: the residual update by a residual s–t assignment.
• TauCeti.Flow cap s t: ordinary s–t flows for the capacities cap.
• TauCeti.Flow.zero: the zero flow for nonnegative capacities.
• TauCeti.BoundedFlow.swapFlow: terminal exchange, turning a capacity-feasible assignment of nonpositive value into an ordinary flow in the opposite direction.
• TauCeti.Flow.augment: augmentation of a flow by a flow of its residual network.

Main results

• TauCeti.BoundedFlow.val_eq_arrowSum_sub: the value is the net value across any terminal-separating vertex set.
• TauCeti.BoundedFlow.val_le_cutBound and TauCeti.BoundedFlow.neg_cutBound_compl_le_val: weak duality for bounded s–t assignments, from above and from below.
• TauCeti.Flow.val_le_arrowSum: weak duality for ordinary flows.
• TauCeti.Flow.arrowSum_le_arrowSum_univ: a flow carries at most the total capacity across any pair of vertex sets.
• TauCeti.map_cutBound: cut bounds commute with additive coefficient maps.
• TauCeti.neg_cutBound_le_sum_excessAt and TauCeti.sum_excessAt_le_cutBound_compl: cut bounds bound the total excess of an assignment between lo and hi on any vertex set.
• TauCeti.BoundedFlow.cutBound_sub_val and TauCeti.BoundedFlow.val_eq_cutBound_iff: the gap between a cut bound and the value is the residual capacity leaving the cut, so the value attains the cut bound exactly when no residual arrow of positive capacity leaves the cut.
• TauCeti.BoundedFlow.val_update and TauCeti.BoundedFlow.exists_update_eq: residual updates add values, and connect any two bounded s–t assignments.
• TauCeti.Flow.exists_augment_eq: every flow of at least the value of f is an augmentation of f by a flow of its residual network.
• TauCeti.Flow.exists_nsmul_eq_val: a flow with arrow values in zmultiples d has value n • d for a natural number n.

References

• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows: Theory, Algorithms, and Applications, Prentice Hall, 1993.
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003.

structure TauCeti.BoundedFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] (lo hi : Assignment Q K) (s t : V) : Type (max (max u v) w)

A bounded s–t assignment for lower and upper bounds lo and hi: an arrow assignment between the bounds, conserved at every vertex other than s and t. There is no sign condition on the arrow values or on the value.

• toFun : Assignment Q K

  The value on each arrow.

• mem_Icc : self.toFun ∈ Set.Icc lo hi

  The assignment lies between the lower and upper bounds.

• conserve (v : V) : v ≠ s → v ≠ t → excessAt self.toFun v = 0

  The assignment is conserved at every vertex other than the terminals.

theorem TauCeti.BoundedFlow.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} {lo hi : Assignment Q K} {s t : V} {x y : BoundedFlow lo hi s t} : x = y ↔ x.toFun = y.toFun

theorem TauCeti.BoundedFlow.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} {lo hi : Assignment Q K} {s t : V} {x y : BoundedFlow lo hi s t} (toFun : x.toFun = y.toFun) : x = y

def TauCeti.cutBound {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] (lo hi : Assignment Q K) (S : Finset V) : K

The cut bound of a vertex set S for lower and upper bounds lo and hi: the total upper bound on arrows leaving S minus the total lower bound on arrows entering S. For zero lower bounds it is the capacity of the arrows leaving S.

theorem TauCeti.cutBound_def {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] (lo hi : Assignment Q K) (S : Finset V) : cutBound lo hi S = arrowSum hi S Sᶜ - arrowSum lo Sᶜ S

@[simp]

theorem TauCeti.cutBound_zero_left {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] (hi : Assignment Q K) (S : Finset V) : cutBound 0 hi S = arrowSum hi S Sᶜ

theorem TauCeti.map_cutBound {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [DecidableEq V] {L : Type u_1} {F : Type u_2} [AddCommGroup L] [FunLike F K L] [AddMonoidHomClass F K L] (φ : F) (lo hi : Assignment Q K) (S : Finset V) : φ (cutBound lo hi S) = cutBound (lo.map ⇑φ) (hi.map ⇑φ) S

Cut bounds commute with additive coefficient maps.

theorem TauCeti.neg_cutBound_le_sum_excessAt {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] [DecidableEq V] {lo hi f : Assignment Q K} (hf : f ∈ Set.Icc lo hi) (S : Finset V) : -cutBound lo hi S ≤ ∑ v ∈ S, excessAt f v

An assignment between lo and hi has total excess on S at least minus the cut bound of S.

theorem TauCeti.sum_excessAt_le_cutBound_compl {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] [DecidableEq V] {lo hi f : Assignment Q K} (hf : f ∈ Set.Icc lo hi) (S : Finset V) : ∑ v ∈ S, excessAt f v ≤ cutBound lo hi Sᶜ

An assignment between lo and hi has total excess on S at most the cut bound of the complement of S.

theorem TauCeti.BoundedFlow.lower_le {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) {x y : V} (e : Q x y) : lo e ≤ f.toFun e

theorem TauCeti.BoundedFlow.le_upper {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) {x y : V} (e : Q x y) : f.toFun e ≤ hi e

def TauCeti.BoundedFlow.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] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) : K

The value of a bounded s–t assignment: its excess at the sink t.

theorem TauCeti.BoundedFlow.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] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) : f.val = excessAt f.toFun t

theorem TauCeti.BoundedFlow.excessAt_source {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) : excessAt f.toFun s = -f.val

The excess at the source is minus the value.

theorem TauCeti.BoundedFlow.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] [Preorder K] {lo hi : Assignment Q K} {s t : V} [DecidableEq V] (f : BoundedFlow lo hi s t) {S : Finset V} (hs : s ∈ S) (ht : t ∉ S) : f.val = arrowSum f.toFun S Sᶜ - arrowSum f.toFun Sᶜ S

The value of a bounded s–t assignment is the value on arrows leaving S minus the value on arrows entering S, for every vertex set S containing s but not t.

theorem TauCeti.BoundedFlow.cutBound_sub_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] {lo hi : Assignment Q K} {s t : V} [DecidableEq V] (f : BoundedFlow lo hi s t) {S : Finset V} (hs : s ∈ S) (ht : t ∉ S) : cutBound lo hi S - f.val = arrowSum (residualCapacity lo hi f.toFun) S Sᶜ

Residual cut gap. For every vertex set S containing s but not t, the cut bound of S exceeds the value of a bounded s–t assignment by its total residual capacity on the residual arrows leaving S: the room left on the arrows leaving S plus the room left to decrease the arrows entering S.

def TauCeti.BoundedFlow.swap {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) : BoundedFlow lo hi t s

A bounded s–t assignment, viewed as a bounded t–s assignment.

@[simp]

theorem TauCeti.BoundedFlow.swap_toFun {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) : f.swap.toFun = f.toFun

@[simp]

theorem TauCeti.BoundedFlow.swap_swap {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) : f.swap.swap = f

@[simp]

theorem TauCeti.BoundedFlow.val_swap {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) : f.swap.val = -f.val

Exchanging the terminals negates the value.

theorem TauCeti.BoundedFlow.val_eq_zero_of_eq {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} (hst : s = t) (f : BoundedFlow lo hi s t) : f.val = 0

A bounded assignment whose terminals coincide has value zero.

theorem TauCeti.BoundedFlow.excessAt_eq_single_sub_single {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {s t : V} [DecidableEq V] (f : BoundedFlow lo hi s t) : excessAt f.toFun = Pi.single t f.val - Pi.single s f.val

The excess of a bounded terminal assignment is concentrated at its terminals, with demand f.val at the sink and supply f.val at the source. This also holds for coinciding terminals.

theorem TauCeti.BoundedFlow.val_le_cutBound {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {lo hi : Assignment Q K} {s t : V} [DecidableEq V] (f : BoundedFlow lo hi s t) {S : Finset V} (hs : s ∈ S) (ht : t ∉ S) : f.val ≤ cutBound lo hi S

Weak duality. The value of a bounded s–t assignment is at most the cut bound of every vertex set containing s but not t.

theorem TauCeti.BoundedFlow.neg_cutBound_compl_le_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] [AddLeftMono K] {lo hi : Assignment Q K} {s t : V} [DecidableEq V] (f : BoundedFlow lo hi s t) {S : Finset V} (hs : s ∈ S) (ht : t ∉ S) : -cutBound lo hi Sᶜ ≤ f.val

Weak duality from below. The value of a bounded s–t assignment is at least minus the cut bound of the complement of every vertex set containing s but not t, that is, at least the total lower bound leaving the set minus the total upper bound entering it.

theorem TauCeti.BoundedFlow.terminal_excess_add_arrowSum_le {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {lo hi : Assignment Q K} {s t : V} [DecidableEq V] (f : BoundedFlow lo hi s t) (S : Finset V) : ((if t ∈ S then f.val else 0) - if s ∈ S then f.val else 0) + arrowSum lo S Sᶜ ≤ arrowSum hi Sᶜ S

The terminal excess of a bounded assignment satisfies the incoming cut inequality on every vertex set, whether or not it separates the terminals.

theorem TauCeti.BoundedFlow.sum_single_sub_single_add_arrowSum_le {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {lo hi : Assignment Q K} {s t : V} [DecidableEq V] (f g : BoundedFlow lo hi s t) {q : K} (hfq : f.val ≤ q) (hqg : q ≤ g.val) (S : Finset V) : ∑ v ∈ S, (Pi.single t q - Pi.single s q) v + arrowSum lo S Sᶜ ≤ arrowSum hi Sᶜ S

A value between two feasible terminal values satisfies every incoming cut inequality for its terminal demand.

def TauCeti.BoundedFlow.update {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) (r : BoundedFlow 0 (residualCapacity lo hi f.toFun) s t) : BoundedFlow lo hi s t

The residual update of a bounded s–t assignment f by a residual s–t assignment r between zero and the residual capacities of f: the value on an arrow e becomes f e + r e⁺ - r e⁻.

@[simp]

theorem TauCeti.BoundedFlow.update_toFun {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) (r : BoundedFlow 0 (residualCapacity lo hi f.toFun) s t) : (f.update r).toFun = residualUpdate f.toFun r.toFun

@[simp]

theorem TauCeti.BoundedFlow.val_update {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) (r : BoundedFlow 0 (residualCapacity lo hi f.toFun) s t) : (f.update r).val = f.val + r.val

A residual update adds the value of the residual assignment.

theorem TauCeti.BoundedFlow.val_eq_cutBound_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] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {s t : V} (f : BoundedFlow lo hi s t) {S : Finset V} (hs : s ∈ S) (ht : t ∉ S) : f.val = cutBound lo hi S ↔ ∀ v ∈ S, ∀ w ∉ S, ∀ (e : ResidualHom Q v w), residualCapacity lo hi f.toFun e = 0

A bounded s–t assignment attains the cut bound of a vertex set S containing s but not t exactly when every residual arrow leaving S has zero residual capacity.

theorem TauCeti.BoundedFlow.exists_update_eq {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {s t : V} (f g : BoundedFlow lo hi s t) : ∃ (r : BoundedFlow 0 (residualCapacity lo hi f.toFun) s t), f.update r = g

Every bounded s–t assignment g is a residual update of any other one f, by a residual s–t assignment, necessarily of value g.val - f.val.

Ordinary flows

structure TauCeti.Flow {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) (s t : V) extends TauCeti.BoundedFlow 0 cap s t : Type (max (max u v) w)

An ordinary s–t flow for the capacities cap: a bounded s–t assignment with zero lower bounds, so with 0 ≤ f e ≤ cap e on every arrow, whose value is nonnegative.

• toFun : Assignment Q K
• mem_Icc : self.toFun ∈ Set.Icc 0 cap
• conserve (v : V) : v ≠ s → v ≠ t → excessAt self.toFun v = 0
• excessAt_sink_nonneg : 0 ≤ excessAt self.toFun t

  The excess at the sink, which is the value of the flow, is nonnegative.

theorem TauCeti.Flow.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} {s t : V} {x y : Flow cap s t} (toFun : x.toFun = y.toFun) : x = y

theorem TauCeti.Flow.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} {s t : V} {x y : Flow cap s t} : x = y ↔ x.toFun = y.toFun

def TauCeti.Flow.zero {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} {s t : V} (hcap : 0 ≤ cap) : Flow cap s t

The zero flow for nonnegative capacities.

@[simp]

theorem TauCeti.Flow.zero_toFun {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} {s t : V} (hcap : 0 ≤ cap) : (zero hcap).toFun = 0

@[simp]

theorem TauCeti.Flow.val_zero {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} {s t : V} (hcap : 0 ≤ cap) : (zero hcap).val = 0

theorem TauCeti.Flow.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} {s t : V} (f : Flow cap s t) {x y : V} (e : Q x y) : 0 ≤ f.toFun e

theorem TauCeti.Flow.val_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} {s t : V} (f : Flow cap s t) : 0 ≤ f.val

def TauCeti.Flow.equivBoundedFlow {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} {s t : V} : Flow cap s t ≃ { f : BoundedFlow 0 cap s t // 0 ≤ f.val }

Ordinary s–t flows are the bounded s–t assignments with zero lower bounds and nonnegative value.

@[simp]

theorem TauCeti.Flow.coe_equivBoundedFlow_apply {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} {s t : V} (f : Flow cap s t) : ↑(equivBoundedFlow f) = f.toBoundedFlow

@[simp]

theorem TauCeti.Flow.toBoundedFlow_equivBoundedFlow_symm_apply {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} {s t : V} (f : { f : BoundedFlow 0 cap s t // 0 ≤ f.val }) : (equivBoundedFlow.symm f).toBoundedFlow = ↑f

def TauCeti.BoundedFlow.swapFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {cap : Assignment Q K} {s t : V} (f : BoundedFlow 0 cap s t) (hf : f.val ≤ 0) : Flow cap t s

Terminal exchange. A capacity-feasible s–t assignment of nonpositive value is an ordinary t–s flow, with the same arrow values and the opposite value.

@[simp]

theorem TauCeti.BoundedFlow.toBoundedFlow_swapFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {cap : Assignment Q K} {s t : V} (f : BoundedFlow 0 cap s t) (hf : f.val ≤ 0) : (f.swapFlow hf).toBoundedFlow = f.swap

theorem TauCeti.Flow.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] [Preorder K] [AddLeftMono K] {cap : Assignment Q K} {s t : V} [DecidableEq V] (f : Flow cap s t) {S : Finset V} (hs : s ∈ S) (ht : t ∉ S) : f.val ≤ arrowSum cap S Sᶜ

Weak duality. The value of an ordinary s–t flow is at most the total capacity of the arrows leaving any vertex set containing s but not t.

def TauCeti.Flow.augment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {cap : Assignment Q K} {s t : V} (f : Flow cap s t) (r : Flow (residualCapacity 0 cap f.toFun) s t) : Flow cap s t

The augmentation of an ordinary s–t flow f by an ordinary s–t flow r of its residual network: the residual update of f by r.

@[simp]

theorem TauCeti.Flow.toBoundedFlow_augment {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Preorder K] [AddLeftMono K] {cap : Assignment Q K} {s t : V} (f : Flow cap s t) (r : Flow (residualCapacity 0 cap f.toFun) s t) : (f.augment r).toBoundedFlow = f.update r.toBoundedFlow

theorem TauCeti.Flow.arrowSum_le_arrowSum_univ {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} (f : Flow cap s t) (S T : Finset V) : arrowSum f.toFun S T ≤ arrowSum cap Finset.univ Finset.univ

The value of an ordinary flow on the arrows from any vertex set to any other is at most the total capacity of all arrows.

theorem TauCeti.Flow.exists_augment_eq {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(v w : V) → Fintype (Q v w)] [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] {cap : Assignment Q K} {s t : V} (f g : Flow cap s t) (hfg : f.val ≤ g.val) : ∃ (r : Flow (residualCapacity 0 cap f.toFun) s t), f.augment r = g

Every ordinary s–t flow g of value at least that of f is the augmentation of f by an ordinary s–t flow of the residual network of f, necessarily of value g.val - f.val.

theorem TauCeti.Flow.exists_nsmul_eq_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] [AddLeftMono K] {cap : Assignment Q K} {s t : V} {d : K} (hd : 0 < d) {f : Flow cap s t} (hf : ∀ ⦃v w : V⦄ (e : Q v w), f.toFun e ∈ AddSubgroup.zmultiples d) : ∃ (n : ℕ), n • d = f.val

For 0 < d, an ordinary flow with arrow values in zmultiples d has value n • d for a natural number n.

Network abbreviations

@[reducible, inline]

abbrev TauCeti.Network.BoundedFlow {V : Type u} {K : Type w} [Fintype V] [AddCommGroup K] [Preorder K] (N : Network K V) [(x y : V) → Fintype (N.Hom x y)] (s t : V) : Type (max (max u u_1) w)

The bounded s–t assignments of a network, respecting both its lower and upper bounds.

@[reducible, inline]

abbrev TauCeti.Network.UpperFlow {V : Type u} {K : Type w} [Fintype V] [AddCommGroup K] [Preorder K] (N : Network K V) [(x y : V) → Fintype (N.Hom x y)] (s t : V) : Type (max (max u u_1) w)

The ordinary s–t flows against the upper bounds of a network. The lower bounds are ignored, so this is the flow type of N only when its lower bounds vanish, as for networks built by Network.ofCapacity.