Residual arrows and the residual update

Let Q be an arrow family on V with lower and upper bounds lo hi : Assignment Q K, and let f be a feasible assignment, lo ≤ f ≤ hi arrowwise; feasibility is membership in the order interval Set.Icc lo hi for the pointwise order on assignments. The residual arrows from v to w are the forward copies e⁺ of the arrows e : Q v w together with the reverse copies e⁻ of the arrows e : Q w v. A forward copy has residual capacity hi e - f e, the room left to increase f e; a reverse copy has residual capacity f e - lo e, the room left to decrease it. The residual arrow family does not depend on f, and zero-capacity residual arrows are retained.

Given any assignment r of the residual arrows, the residual update of f by r is f' e = f e + r e⁺ - r e⁻. Augmentation along residual paths and cycles is the case of a residual assignment supported on a path or cycle, for ordinary flows as well as for assignments with signed lower bounds. We prove:

• if 0 ≤ r ≤ the residual capacities, then f' is feasible;
• excessAt f' = excessAt f + excessAt r at every vertex, with no conservation hypothesis on r; so a residual circulation preserves every excess, and a residual s–t assignment changes the excess only at s and t, raising it at t and lowering it at s by its value;
• conversely every feasible assignment g is the residual update of f by the residual difference from f to g, the positive part of g - f on forward copies and its negative part on reverse copies; this residual assignment is feasible, its values on the two copies of an arrow have infimum zero (so in a linear order one of them vanishes), and it has excess excessAt g - excessAt f. So the feasible residual updates of f are exactly the feasible assignments, and two assignments of the same excess differ by a residual circulation.

Main definitions

• TauCeti.ResidualHom Q: the residual arrow family fun v w ↦ Q v w ⊕ Q w v.
• TauCeti.residualCapacity lo hi f: the residual capacities of f.
• TauCeti.residualNet: the net change r e⁺ - r e⁻ of a residual assignment, as an additive homomorphism.
• TauCeti.residualUpdate f r: the residual update f + residualNet r.
• TauCeti.residualDifference f g: the canonical residual assignment updating f to g.

Main results

• TauCeti.excessAt_residualNet: passing from residual arrows to net changes preserves excess.
• TauCeti.residualUpdate_mem_Icc: feasible residual updates are feasible.
• TauCeti.excessAt_residualUpdate: excess is additive under residual updates.
• TauCeti.residualCapacity_residualUpdate: the residual capacities after a residual update.
• TauCeti.excessAt_residualUpdate_source: a residual assignment conserved away from s and t lowers the excess at s by its value at t.
• TauCeti.residualUpdate_residualDifference, TauCeti.residualDifference_mem_Icc and TauCeti.excessAt_residualDifference: the residual difference updates f to g, is feasible for feasible f and g, and changes excess by the difference of the excesses.
• TauCeti.image_residualUpdate_Icc: the residual updates of a feasible f by feasible residual assignments are exactly the feasible assignments.
• TauCeti.Assignment.map_residualCapacity and TauCeti.Assignment.map_residualUpdate: residual capacities and residual updates commute with additive coefficient maps.

Implementation notes

The residual arrows are tagged by Sum.inl (forward) and Sum.inr (reverse) rather than by their direction relative to the original arrow family, so that a forward copy of an arrow v → w and a reverse copy of an antiparallel arrow w → v remain distinct residual arrows from v to w, as do the two residual copies of a loop. Bounds are separate parameters, so the results apply to any arrow family carrying lower and upper bounds.

References

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

@[reducible, inline]

abbrev TauCeti.ResidualHom {V : Type u} (Q : V → V → Type v) (v w : V) : Type v

The residual arrow family of Q: a residual arrow from v to w is either a forward copy Sum.inl e of an arrow e : Q v w or a reverse copy Sum.inr e of an arrow e : Q w v.

def TauCeti.residualCapacity {V : Type u} {Q : V → V → Type v} {K : Type w} [Sub K] (lo hi f : Assignment Q K) : Assignment (ResidualHom Q) K

The residual capacities of an assignment f with lower and upper bounds lo and hi: the forward copy of an arrow e has capacity hi e - f e and its reverse copy has capacity f e - lo e.

@[simp]

theorem TauCeti.residualCapacity_inl {V : Type u} {Q : V → V → Type v} {K : Type w} [Sub K] (lo hi f : Assignment Q K) {v w : V} (e : Q v w) : residualCapacity lo hi f (Sum.inl e) = hi e - f e

@[simp]

theorem TauCeti.residualCapacity_inr {V : Type u} {Q : V → V → Type v} {K : Type w} [Sub K] (lo hi f : Assignment Q K) {v w : V} (e : Q w v) : residualCapacity lo hi f (Sum.inr e) = f e - lo e

theorem TauCeti.Assignment.map_residualCapacity {V : Type u} {Q : V → V → Type v} {K : Type w} [AddGroup K] {L : Type u_1} {F : Type u_2} [SubtractionMonoid L] [FunLike F K L] [AddMonoidHomClass F K L] (φ : F) (lo hi f : Assignment Q K) : (residualCapacity lo hi f).map ⇑φ = residualCapacity (lo.map ⇑φ) (hi.map ⇑φ) (f.map ⇑φ)

Residual capacities commute with additive coefficient maps.

theorem TauCeti.residualCapacity_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [AddGroup K] {S : Type u_1} [SetLike S K] [AddSubgroupClass S K] (H : S) {lo hi f : Assignment Q K} (hlo : ∀ ⦃v w : V⦄ (e : Q v w), lo e ∈ H) (hhi : ∀ ⦃v w : V⦄ (e : Q v w), hi e ∈ H) (hf : ∀ ⦃v w : V⦄ (e : Q v w), f e ∈ H) {v w : V} (e : ResidualHom Q v w) : residualCapacity lo hi f e ∈ H

Residual capacities take values in an additive subgroup containing the bounds and the assignment.

theorem TauCeti.residualCapacity_nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [AddGroup K] [Preorder K] [AddRightMono K] {lo hi f : Assignment Q K} (hf : f ∈ Set.Icc lo hi) : 0 ≤ residualCapacity lo hi f

The residual capacities of a feasible assignment are nonnegative.

theorem TauCeti.arrowSum_residualCapacity {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommMonoid K] [Sub K] [(v w : V) → Fintype (Q v w)] (lo hi f : Assignment Q K) (S T : Finset V) : arrowSum (residualCapacity lo hi f) S T = arrowSum (hi - f) S T + arrowSum (f - lo) T S

The residual capacity on the residual arrows from S to T is the room left on the arrows from S to T plus the room left to decrease the arrows from T to S.

def TauCeti.residualNet {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] : Assignment (ResidualHom Q) K →+ Assignment Q K

The net change of a residual assignment r: the value of r on the forward copy of an arrow minus its value on the reverse copy.

@[simp]

theorem TauCeti.residualNet_apply {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] (r : Assignment (ResidualHom Q) K) {v w : V} (e : Q v w) : residualNet r e = r (Sum.inl e) - r (Sum.inr e)

def TauCeti.residualUpdate {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] (f : Assignment Q K) (r : Assignment (ResidualHom Q) K) : Assignment Q K

The residual update of f by a residual assignment r: the value on each arrow e is f e + r e⁺ - r e⁻, where e⁺ = Sum.inl e and e⁻ = Sum.inr e are its residual copies.

theorem TauCeti.residualUpdate_def {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] (f : Assignment Q K) (r : Assignment (ResidualHom Q) K) : residualUpdate f r = f + residualNet r

@[simp]

theorem TauCeti.residualUpdate_apply {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] (f : Assignment Q K) (r : Assignment (ResidualHom Q) K) {v w : V} (e : Q v w) : residualUpdate f r e = f e + r (Sum.inl e) - r (Sum.inr e)

@[simp]

theorem TauCeti.residualUpdate_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] (f : Assignment Q K) : residualUpdate f 0 = f

theorem TauCeti.residualUpdate_residualUpdate {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] (f : Assignment Q K) (r r' : Assignment (ResidualHom Q) K) : residualUpdate (residualUpdate f r) r' = residualUpdate f (r + r')

Updating by r and then by r' is updating by r + r'.

theorem TauCeti.Assignment.map_residualNet {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] {L : Type u_1} {F : Type u_2} [AddCommGroup L] [FunLike F K L] [AddMonoidHomClass F K L] (φ : F) (r : Assignment (ResidualHom Q) K) : (residualNet r).map ⇑φ = residualNet (r.map ⇑φ)

theorem TauCeti.Assignment.map_residualUpdate {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] {L : Type u_1} {F : Type u_2} [AddCommGroup L] [FunLike F K L] [AddMonoidHomClass F K L] (φ : F) (f : Assignment Q K) (r : Assignment (ResidualHom Q) K) : (residualUpdate f r).map ⇑φ = residualUpdate (f.map ⇑φ) (r.map ⇑φ)

Residual updates commute with additive coefficient maps.

theorem TauCeti.residualUpdate_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] {S : Type u_1} [SetLike S K] [AddSubgroupClass S K] (H : S) {f : Assignment Q K} {r : Assignment (ResidualHom Q) K} (hf : ∀ ⦃v w : V⦄ (e : Q v w), f e ∈ H) (hr : ∀ ⦃v w : V⦄ (e : ResidualHom Q v w), r e ∈ H) {v w : V} (e : Q v w) : residualUpdate f r e ∈ H

Residual updates preserve values in an additive subgroup: if f and r take values in H, so does the residual update of f by r.

theorem TauCeti.residualCapacity_residualUpdate {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] (lo hi f : Assignment Q K) (r : Assignment (ResidualHom Q) K) {v w : V} (a : ResidualHom Q v w) : residualCapacity lo hi (residualUpdate f r) a = residualCapacity lo hi f a - r a + r (Sum.swap a)

Residual capacities after a residual update. Updating f by r lowers the residual capacity of a residual arrow a by the value of r on a and raises it by the value of r on the reverse residual arrow a.swap, the other residual copy of the same arrow.

@[simp]

theorem TauCeti.excessAt_residualNet {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Fintype V] [(v w : V) → Fintype (Q v w)] (r : Assignment (ResidualHom Q) K) (v : V) : excessAt (residualNet r) v = excessAt r v

Passing from a residual assignment to its net change preserves excess: a forward copy carries value along its arrow, and a reverse copy carries value against it.

@[simp]

theorem TauCeti.excessAt_residualUpdate {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Fintype V] [(v w : V) → Fintype (Q v w)] (f : Assignment Q K) (r : Assignment (ResidualHom Q) K) (v : V) : excessAt (residualUpdate f r) v = excessAt f v + excessAt r v

Excess under residual updates. The excess of the residual update of f by r is the excess of f plus the excess of r in the residual arrow family. No conservation is assumed.

theorem TauCeti.IsCirculation.excessAt_residualUpdate {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Fintype V] [(v w : V) → Fintype (Q v w)] {r : Assignment (ResidualHom Q) K} (hr : IsCirculation r) (f : Assignment Q K) (v : V) : excessAt (residualUpdate f r) v = excessAt f v

A residual circulation preserves every excess.

theorem TauCeti.excessAt_residualUpdate_source {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Fintype V] [(v w : V) → Fintype (Q v w)] {r : Assignment (ResidualHom Q) K} {s t : V} (hconserve : ∀ (v : V), v ≠ s → v ≠ t → excessAt r v = 0) (f : Assignment Q K) : excessAt (residualUpdate f r) s = excessAt f s - excessAt r t

A residual assignment conserved away from s and t lowers the excess at s by its excess at t. Together with excessAt_residualUpdate at t, the value of an s–t assignment rises by the residual value, and the value of the reversed t–s assignment falls by it.

theorem TauCeti.residualUpdate_mem_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Preorder K] [AddLeftMono K] {lo hi f : Assignment Q K} {r : Assignment (ResidualHom Q) K} (hr : r ∈ Set.Icc 0 (residualCapacity lo hi f)) : residualUpdate f r ∈ Set.Icc lo hi

Feasibility of residual updates. Updating an assignment by a residual assignment between zero and its residual capacities gives an assignment within the bounds. Such a residual assignment exists only when the residual capacities are nonnegative, that is, when f is itself feasible.

def TauCeti.residualDifference {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] (f g : Assignment Q K) : Assignment (ResidualHom Q) K

The residual difference from f to g: the positive part of g - f on the forward copy of each arrow and its negative part on the reverse copy. It is the canonical residual assignment updating f to g, and its values on the two residual copies of an arrow have infimum zero.

@[simp]

theorem TauCeti.residualDifference_inl {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] (f g : Assignment Q K) {v w : V} (e : Q v w) : residualDifference f g (Sum.inl e) = (g e - f e)⁺

@[simp]

theorem TauCeti.residualDifference_inr {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] (f g : Assignment Q K) {v w : V} (e : Q w v) : residualDifference f g (Sum.inr e) = (g e - f e)⁻

@[simp]

theorem TauCeti.residualDifference_self {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] (f : Assignment Q K) : residualDifference f f = 0

theorem TauCeti.residualDifference_nonneg {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] (f g : Assignment Q K) : 0 ≤ residualDifference f g

@[simp]

theorem TauCeti.residualNet_residualDifference {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] (f g : Assignment Q K) : residualNet (residualDifference f g) = g - f

The net change of the residual difference from f to g is g - f.

@[simp]

theorem TauCeti.residualUpdate_residualDifference {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] (f g : Assignment Q K) : residualUpdate f (residualDifference f g) = g

Residual update by the residual difference. Updating f by the residual difference from f to g gives g.

theorem TauCeti.residualDifference_inl_inf_inr {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] (f g : Assignment Q K) {v w : V} (e : Q v w) : residualDifference f g (Sum.inl e) ⊓ residualDifference f g (Sum.inr e) = 0

The values of the residual difference on the two residual copies of an arrow have infimum zero; in a linear order, at least one of them vanishes.

theorem TauCeti.residualDifference_mem_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] {lo hi f g : Assignment Q K} (hf : f ∈ Set.Icc lo hi) (hg : g ∈ Set.Icc lo hi) : residualDifference f g ∈ Set.Icc 0 (residualCapacity lo hi f)

The residual difference between two feasible assignments lies between zero and the residual capacities of the first.

theorem TauCeti.exists_residualUpdate_eq {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] {lo hi f g : Assignment Q K} (hf : f ∈ Set.Icc lo hi) (hg : g ∈ Set.Icc lo hi) : ∃ r ∈ Set.Icc 0 (residualCapacity lo hi f), residualUpdate f r = g

Completeness of residual updates. Every feasible assignment g is the residual update of a feasible f by a residual assignment between zero and the residual capacities of f, namely the residual difference from f to g.

theorem TauCeti.image_residualUpdate_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] {lo hi f : Assignment Q K} (hf : f ∈ Set.Icc lo hi) : residualUpdate f '' Set.Icc 0 (residualCapacity lo hi f) = Set.Icc lo hi

The residual updates of a feasible assignment f by residual assignments between zero and its residual capacities are exactly the feasible assignments.

@[simp]

theorem TauCeti.excessAt_residualDifference {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] (f g : Assignment Q K) (v : V) : excessAt (residualDifference f g) v = excessAt g v - excessAt f v

Excess of the residual difference. The excess of the residual difference from f to g is the excess of g minus the excess of f.

theorem TauCeti.isCirculation_residualDifference {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [Lattice K] [IsOrderedAddMonoid K] [Fintype V] [(v w : V) → Fintype (Q v w)] {f g : Assignment Q K} (hfg : ∀ (v : V), excessAt f v = excessAt g v) : IsCirculation (residualDifference f g)

The residual difference between two assignments with the same excess is a residual circulation.

theorem TauCeti.residualDifference_mem {V : Type u} {Q : V → V → Type v} {K : Type w} [AddCommGroup K] [LinearOrder K] {S : Type u_1} [SetLike S K] [AddSubgroupClass S K] (H : S) {f g : Assignment Q K} (hf : ∀ ⦃v w : V⦄ (e : Q v w), f e ∈ H) (hg : ∀ ⦃v w : V⦄ (e : Q v w), g e ∈ H) {v w : V} (e : ResidualHom Q v w) : residualDifference f g e ∈ H

The residual difference between two assignments with values in an additive subgroup takes values in it.