Shifting bounded assignments and prescribed excess

Subtracting a reference assignment translates both arrow bounds and vertex excess. The reference need not be feasible. This gives equivalences for exact and interval excess problems and, by subtracting the lower bound, reduces signed bounds to nonnegative capacities. Subtracting a feasible reference instead reduces its prescribed-excess problem to a circulation problem.

ExcessFlow and ExcessIntervalFlow use the same arrow assignments and interval bounds as BoundedFlow; their extra constraint prescribes excess at every vertex. Excess is incoming minus outgoing, so the shifted demand is the original demand minus the reference excess.

References

• D. P. Bertsekas, Linear Network Optimization, Section 1.1.3 and Exercises 2.4–2.6.

@[reducible, inline]

abbrev TauCeti.ExcessFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] (lo hi : Assignment Q K) (b : V → K) : Type (max 0 (max u v) w)

Arrow assignments between lo and hi whose excess is the prescribed function b. Positive excess denotes demand; negative excess denotes supply.

@[reducible, inline]

abbrev TauCeti.ExcessIntervalFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] (lo hi : Assignment Q K) (a b : V → K) : Type (max 0 (max u v) w)

Arrow assignments between lo and hi whose excess lies between a and b. The vertex bounds constrain net excess, rather than total traffic through a vertex.

theorem TauCeti.ExcessFlow.mem_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {b : V → K} (f : ExcessFlow lo hi b) : ↑f ∈ Set.Icc lo hi

A realizing assignment respects its arrow bounds.

@[simp]

theorem TauCeti.ExcessFlow.excessAt_eq {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {b : V → K} (f : ExcessFlow lo hi b) (x : V) : excessAt (↑f) x = b x

A realizing assignment has the prescribed excess at each vertex.

theorem TauCeti.ExcessFlow.sum_eq_zero_of_forall_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {b : V → K} (f : ExcessFlow lo hi b) {S : Finset V} (hS : ∀ ⦃x y : V⦄ (a : Q x y), x ∈ S ↔ y ∈ S) : ∑ v ∈ S, b v = 0

On a vertex set that no arrow enters or leaves, such as a weakly connected component, the prescribed excess of a feasible assignment has total zero.

theorem TauCeti.ExcessFlow.sum_eq_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {b : V → K} (f : ExcessFlow lo hi b) : ∑ v : V, b v = 0

Prescribed excess of a feasible assignment has total zero.

theorem TauCeti.ExcessFlow.sum_add_arrowSum_le {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] [AddLeftMono K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (f : ExcessFlow lo hi b) (S : Finset V) : ∑ v ∈ S, b v + arrowSum lo S Sᶜ ≤ arrowSum hi Sᶜ S

Every feasible prescribed-excess assignment satisfies the incoming cut inequality.

theorem TauCeti.ExcessIntervalFlow.mem_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {a b : V → K} (f : ExcessIntervalFlow lo hi a b) : ↑f ∈ Set.Icc lo hi

An interval-excess assignment respects its arrow bounds.

theorem TauCeti.ExcessIntervalFlow.excessAt_mem_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [Preorder K] {lo hi : Assignment Q K} {a b : V → K} (f : ExcessIntervalFlow lo hi a b) : excessAt ↑f ∈ Set.Icc a b

An interval-excess assignment respects its vertex bounds.

theorem TauCeti.ExcessIntervalFlow.sum_le_zero_of_forall_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {a b : V → K} (f : ExcessIntervalFlow lo hi a b) {S : Finset V} (hS : ∀ ⦃x y : V⦄ (a : Q x y), x ∈ S ↔ y ∈ S) : ∑ v ∈ S, a v ≤ 0

On a vertex set that no arrow enters or leaves, such as a weakly connected component, the lower vertex bounds have nonpositive total.

theorem TauCeti.ExcessIntervalFlow.zero_le_sum_of_forall_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {a b : V → K} (f : ExcessIntervalFlow lo hi a b) {S : Finset V} (hS : ∀ ⦃x y : V⦄ (a : Q x y), x ∈ S ↔ y ∈ S) : 0 ≤ ∑ v ∈ S, b v

On a vertex set that no arrow enters or leaves, such as a weakly connected component, the upper vertex bounds have nonnegative total.

theorem TauCeti.ExcessIntervalFlow.sum_le_zero {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {a b : V → K} (f : ExcessIntervalFlow lo hi a b) : ∑ v : V, a v ≤ 0

The lower vertex bounds of a feasible problem have nonpositive total.

theorem TauCeti.ExcessIntervalFlow.zero_le_sum {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {a b : V → K} (f : ExcessIntervalFlow lo hi a b) : 0 ≤ ∑ v : V, b v

The upper vertex bounds of a feasible problem have nonnegative total.

def TauCeti.ExcessIntervalFlow.shiftEquiv {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi h : Assignment Q K) (a b : V → K) : ExcessIntervalFlow lo hi a b ≃ ExcessIntervalFlow (lo - h) (hi - h) (a - excessAt h) (b - excessAt h)

Subtract a reference assignment, shifting both endpoints of the vertex-excess intervals.

@[simp]

theorem TauCeti.ExcessIntervalFlow.shiftEquiv_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi h : Assignment Q K) (a b : V → K) (f : ExcessIntervalFlow lo hi a b) : ↑((shiftEquiv lo hi h a b) f) = ↑f - h

@[simp]

theorem TauCeti.ExcessIntervalFlow.shiftEquiv_symm_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi h : Assignment Q K) (a b : V → K) (f : ExcessIntervalFlow (lo - h) (hi - h) (a - excessAt h) (b - excessAt h)) : ↑((shiftEquiv lo hi h a b).symm f) = ↑f + h

theorem TauCeti.ExcessIntervalFlow.shiftEquiv_apply_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi h : Assignment Q K) (a b : V → K) {M : Type u_1} [SetLike M K] [AddSubgroupClass M K] (H : M) (hh : ∀ ⦃x y : V⦄ (e : Q x y), h e ∈ H) (f : ExcessIntervalFlow lo hi a b) {x y : V} (e : Q x y) : ↑((shiftEquiv lo hi h a b) f) e ∈ H ↔ ↑f e ∈ H

Interval-excess shifts also preserve any additive subgroup containing the reference.

def TauCeti.ExcessIntervalFlow.equivExcessFlow {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] (lo hi : Assignment Q K) (b : V → K) : ExcessIntervalFlow lo hi b b ≃ ExcessFlow lo hi b

Equal excess endpoints give exactly the prescribed-excess problem, with the same assignment.

@[simp]

theorem TauCeti.ExcessIntervalFlow.equivExcessFlow_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] (lo hi : Assignment Q K) (b : V → K) (f : ExcessIntervalFlow lo hi b b) : ↑((equivExcessFlow lo hi b) f) = ↑f

@[simp]

theorem TauCeti.ExcessIntervalFlow.equivExcessFlow_symm_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] (lo hi : Assignment Q K) (b : V → K) (f : ExcessFlow lo hi b) : ↑((equivExcessFlow lo hi b).symm f) = ↑f

def TauCeti.ExcessFlow.shiftEquiv {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi h : Assignment Q K) (b : V → K) : ExcessFlow lo hi b ≃ ExcessFlow (lo - h) (hi - h) (b - excessAt h)

Subtract an arbitrary reference assignment, shifting arrow bounds and prescribed excess. The inverse adds the reference assignment.

@[simp]

theorem TauCeti.ExcessFlow.shiftEquiv_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi h : Assignment Q K) (b : V → K) (f : ExcessFlow lo hi b) : ↑((shiftEquiv lo hi h b) f) = ↑f - h

@[simp]

theorem TauCeti.ExcessFlow.shiftEquiv_symm_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi h : Assignment Q K) (b : V → K) (f : ExcessFlow (lo - h) (hi - h) (b - excessAt h)) : ↑((shiftEquiv lo hi h b).symm f) = ↑f + h

theorem TauCeti.ExcessFlow.shiftEquiv_apply_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi h : Assignment Q K) (b : V → K) {M : Type u_1} [SetLike M K] [AddSubgroupClass M K] (H : M) (hh : ∀ ⦃x y : V⦄ (e : Q x y), h e ∈ H) (f : ExcessFlow lo hi b) {x y : V} (e : Q x y) : ↑((shiftEquiv lo hi h b) f) e ∈ H ↔ ↑f e ∈ H

A shift by a subgroup-valued reference preserves subgroup membership arrowwise.

def TauCeti.ExcessFlow.shiftLowerEquiv {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi : Assignment Q K) (b : V → K) : ExcessFlow lo hi b ≃ ExcessFlow 0 (hi - lo) (b - excessAt lo)

Subtracting the lower bound turns the arrow constraints into ordinary capacity constraints.

@[simp]

theorem TauCeti.ExcessFlow.shiftLowerEquiv_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi : Assignment Q K) (b : V → K) (f : ExcessFlow lo hi b) : ↑((shiftLowerEquiv lo hi b) f) = ↑f - lo

@[simp]

theorem TauCeti.ExcessFlow.shiftLowerEquiv_symm_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] (lo hi : Assignment Q K) (b : V → K) (f : ExcessFlow 0 (hi - lo) (b - excessAt lo)) : ↑((shiftLowerEquiv lo hi b).symm f) = ↑f + lo

def TauCeti.ExcessFlow.circulationEquiv {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {b : V → K} (h : ExcessFlow lo hi b) : ExcessFlow lo hi b ≃ { f : Assignment Q K // f ∈ Set.Icc (lo - ↑h) (hi - ↑h) ∧ IsCirculation f }

Relative to a feasible reference, the prescribed-excess problem is a circulation problem.

@[simp]

theorem TauCeti.ExcessFlow.circulationEquiv_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {b : V → K} (h f : ExcessFlow lo hi b) : ↑(h.circulationEquiv f) = ↑f - ↑h

@[simp]

theorem TauCeti.ExcessFlow.circulationEquiv_symm_apply_val {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [PartialOrder K] [IsOrderedAddMonoid K] {lo hi : Assignment Q K} {b : V → K} (h : ExcessFlow lo hi b) (f : { f : Assignment Q K // f ∈ Set.Icc (lo - ↑h) (hi - ↑h) ∧ IsCirculation f }) : ↑(h.circulationEquiv.symm f) = ↑f + ↑h

Signed-bound examples