Interval excess as bounded circulation

Adjoin one fresh vertex to a directed network and one arrow from each original vertex to the fresh vertex. Giving that arrow the original vertex's excess turns an interval-excess assignment into a circulation; its bounds are precisely the bounds on vertex excess. Restriction to the original arrows is the inverse. Negative bounds, parallel arrows and loops are allowed.

ExcessIntervalFlow.circulationEquiv preserves every original arrow value. Conservation at the fresh vertex follows from sum_excessAt, including when the original vertex type is empty.

Hoffman's theorem on the enlarged network gives the feasibility criterion: for ordered bounds, an assignment with excess between a and b exists exactly when every vertex set S satisfies a(S) ≤ cutBound lo hi Sᶜ and -cutBound lo hi S ≤ b(S). A vertex set violating one of these inequalities certifies infeasibility, and bounds in an additive subgroup give a solution in that subgroup. The totals a(V) ≤ 0 ≤ b(V), and the same inequalities on every weakly connected component, are necessary but not sufficient. Equal endpoints recover prescribed excess.

References

• D. P. Bertsekas, Linear Network Optimization, Section 1.1.3 and Exercises 2.4–2.6.
• D. Gale, A theorem on flows in networks, Pacific J. Math. 7 (1957), 1073–1082.

def TauCeti.IntervalExcessHom {V : Type u} (Q : V → V → Type v) : Option V → Option V → Type v

The original arrows between vertices some v, with one arrow from each some v to the fresh vertex none and no arrows leaving none. The family is exposed to identify its indexed arrow carriers with the original carriers.

@[instance_reducible]

instance TauCeti.IntervalExcessHom.instFintype {V : Type u} {Q : V → V → Type v} [(x y : V) → Fintype (Q x y)] (x y : Option V) : Fintype (IntervalExcessHom Q x y)

def TauCeti.IntervalExcessHom.original {V : Type u} {Q : V → V → Type v} {x y : V} (e : Q x y) : IntervalExcessHom Q (some x) (some y)

An original arrow in the enlarged network.

def TauCeti.IntervalExcessHom.auxiliary {V : Type u} {Q : V → V → Type v} (v : V) : IntervalExcessHom Q (some v) none

The auxiliary arrow from some v to none.

instance TauCeti.IntervalExcessHom.instSubsingletonAuxiliary {V : Type u} {Q : V → V → Type v} (v : V) : Subsingleton (IntervalExcessHom Q (some v) none)

instance TauCeti.IntervalExcessHom.instIsEmptyFromNone {V : Type u} {Q : V → V → Type v} (y : Option V) : IsEmpty (IntervalExcessHom Q none y)

No arrow leaves the fresh vertex.

theorem TauCeti.IntervalExcessHom.forall_iff {V : Type u} {Q : V → V → Type v} {P : ⦃x y : Option V⦄ → IntervalExcessHom Q x y → Prop} : (∀ ⦃x y : Option V⦄ (e : IntervalExcessHom Q x y), P e) ↔ (∀ ⦃x y : V⦄ (e : Q x y), P (original e)) ∧ ∀ (v : V), P (auxiliary v)

A property of all enlarged arrows is a property of the original and auxiliary arrows.

def TauCeti.intervalExcessExtend {V : Type u} {Q : V → V → Type v} {K : Type w} (f : Assignment Q K) (c : V → K) : Assignment (IntervalExcessHom Q) K

Extend an original assignment by giving the auxiliary arrow at v the value c v. This also extends lower and upper bounds.

def TauCeti.intervalExcessRestrict {V : Type u} {Q : V → V → Type v} {K : Type w} (g : Assignment (IntervalExcessHom Q) K) : Assignment Q K

Restrict an enlarged assignment to the original arrows.

@[simp]

theorem TauCeti.intervalExcessExtend_original {V : Type u} {Q : V → V → Type v} {K : Type w} (f : Assignment Q K) (c : V → K) {x y : V} (e : Q x y) : intervalExcessExtend f c (IntervalExcessHom.original e) = f e

@[simp]

theorem TauCeti.intervalExcessExtend_auxiliary {V : Type u} {Q : V → V → Type v} {K : Type w} (f : Assignment Q K) (c : V → K) (v : V) : intervalExcessExtend f c (IntervalExcessHom.auxiliary v) = c v

@[simp]

theorem TauCeti.intervalExcessRestrict_apply {V : Type u} {Q : V → V → Type v} {K : Type w} (g : Assignment (IntervalExcessHom Q) K) {x y : V} (e : Q x y) : intervalExcessRestrict g e = g (IntervalExcessHom.original e)

@[simp]

theorem TauCeti.intervalExcessRestrict_extend {V : Type u} {Q : V → V → Type v} {K : Type w} (f : Assignment Q K) (c : V → K) : intervalExcessRestrict (intervalExcessExtend f c) = f

theorem TauCeti.intervalExcessExtend_restrict {V : Type u} {Q : V → V → Type v} {K : Type w} (g : Assignment (IntervalExcessHom Q) K) : (intervalExcessExtend (intervalExcessRestrict g) fun (v : V) => g (IntervalExcessHom.auxiliary v)) = g

Restriction together with the values on auxiliary arrows determines the full assignment.

theorem TauCeti.intervalExcessExtend_mem_Icc {V : Type u} {Q : V → V → Type v} {K : Type w} [Preorder K] (f lo hi : Assignment Q K) (c a b : V → K) : intervalExcessExtend f c ∈ Set.Icc (intervalExcessExtend lo a) (intervalExcessExtend hi b) ↔ f ∈ Set.Icc lo hi ∧ c ∈ Set.Icc a b

The enlarged bounds impose the original arrow bounds and the auxiliary vertex bounds.

@[reducible]

def TauCeti.Network.intervalExcess {V : Type u} {K : Type w} [LE K] (N : Network K V) (a b : V → K) (hab : a ≤ b) : Network K (Option V)

Enlarge a bounded network by one fresh vertex and auxiliary arrows with bounds [a v, b v]. The dependent arrow family is reducible so callers can use the same original and auxiliary arrows in the bundled and unbundled presentations.

@[simp]

theorem TauCeti.Network.intervalExcess_Hom {V : Type u} {K : Type w} [LE K] (N : Network K V) (a b : V → K) (hab : a ≤ b) : (N.intervalExcess a b hab).Hom = IntervalExcessHom N.Hom

@[simp]

theorem TauCeti.Network.intervalExcess_lower {V : Type u} {K : Type w} [LE K] (N : Network K V) (a b : V → K) (hab : a ≤ b) : (N.intervalExcess a b hab).lower = intervalExcessExtend N.lower a

@[simp]

theorem TauCeti.Network.intervalExcess_upper {V : Type u} {K : Type w} [LE K] (N : Network K V) (a b : V → K) (hab : a ≤ b) : (N.intervalExcess a b hab).upper = intervalExcessExtend N.upper b

theorem TauCeti.arrowSum_intervalExcessExtend {V : Type u} {Q : V → V → Type v} {K : Type w} [(x y : V) → Fintype (Q x y)] [AddCommMonoid K] [DecidableEq V] (f : Assignment Q K) (c : V → K) (S T : Finset (Option V)) : arrowSum (intervalExcessExtend f c) S T = arrowSum f (Finset.eraseNone S) (Finset.eraseNone T) + if none ∈ T then ∑ v ∈ Finset.eraseNone S, c v else 0

Arrow sums in the enlarged network: the original arrows contribute their original arrow sum, and when T contains the fresh vertex, the auxiliary arrow at each original vertex of S contributes its value.

theorem TauCeti.IntervalExcessHom.excessAt_some {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] (g : Assignment (IntervalExcessHom Q) K) (v : V) : excessAt g (some v) = excessAt (intervalExcessRestrict g) v - g (auxiliary v)

At an original vertex, enlarged excess is original excess minus the auxiliary value.

theorem TauCeti.IntervalExcessHom.excessAt_none {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] (g : Assignment (IntervalExcessHom Q) K) : excessAt g none = ∑ v : V, g (auxiliary v)

Excess at the fresh vertex is the total value of the auxiliary arrows.

theorem TauCeti.IntervalExcessHom.auxiliary_eq_excessAt {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] {g : Assignment (IntervalExcessHom Q) K} (hg : IsCirculation g) (v : V) : g (auxiliary v) = excessAt (intervalExcessRestrict g) v

Conservation at the original vertices forces each auxiliary value to equal original excess.

theorem TauCeti.isCirculation_intervalExcessExtend {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] (f : Assignment Q K) : IsCirculation (intervalExcessExtend f (excessAt f))

Sending original excess along each auxiliary arrow gives a circulation.

def TauCeti.ExcessIntervalFlow.circulationEquiv {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) : ExcessIntervalFlow lo hi a b ≃ ExcessFlow (intervalExcessExtend lo a) (intervalExcessExtend hi b) 0

An interval-excess assignment is equivalently a bounded circulation on the network with one fresh vertex. The auxiliary arrow at each vertex carries that vertex's original excess.

@[simp]

theorem TauCeti.ExcessIntervalFlow.circulationEquiv_apply_original {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) {x y : V} (e : Q x y) : ↑((circulationEquiv lo hi a b) f) (IntervalExcessHom.original e) = ↑f e

@[simp]

theorem TauCeti.ExcessIntervalFlow.circulationEquiv_apply_auxiliary {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) (v : V) : ↑((circulationEquiv lo hi a b) f) (IntervalExcessHom.auxiliary v) = excessAt (↑f) v

@[simp]

theorem TauCeti.ExcessIntervalFlow.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] [Preorder K] (lo hi : Assignment Q K) (a b : V → K) (g : ExcessFlow (intervalExcessExtend lo a) (intervalExcessExtend hi b) 0) : ↑((circulationEquiv lo hi a b).symm g) = intervalExcessRestrict ↑g

Feasibility of interval excess

theorem TauCeti.ExcessIntervalFlow.sum_le_cutBound_compl {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} [DecidableEq V] (f : ExcessIntervalFlow lo hi a b) (S : Finset V) : ∑ v ∈ S, a v ≤ cutBound lo hi Sᶜ

In a feasible interval-excess problem, the lower vertex bounds on any vertex set are at most the cut bound of its complement.

theorem TauCeti.ExcessIntervalFlow.neg_cutBound_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} [DecidableEq V] (f : ExcessIntervalFlow lo hi a b) (S : Finset V) : -cutBound lo hi S ≤ ∑ v ∈ S, b v

In a feasible interval-excess problem, the upper vertex bounds on any vertex set are at least minus its cut bound.

theorem TauCeti.ExcessIntervalFlow.exists_mem_of_forall_cutBound {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {a b : V → K} (hlo : lo ≤ hi) (hab : a ≤ b) (ha : ∀ (S : Finset V), ∑ v ∈ S, a v ≤ cutBound lo hi Sᶜ) (hb : ∀ (S : Finset V), -cutBound lo hi S ≤ ∑ v ∈ S, b v) (H : AddSubgroup K) (hloH : ∀ ⦃x y : V⦄ (e : Q x y), lo e ∈ H) (hhiH : ∀ ⦃x y : V⦄ (e : Q x y), hi e ∈ H) (haH : ∀ (v : V), a v ∈ H) (hbH : ∀ (v : V), b v ∈ H) : ∃ (f : ExcessIntervalFlow lo hi a b), ∀ ⦃x y : V⦄ (e : Q x y), ↑f e ∈ H

Integrality of interval-excess feasibility. If the arrow and vertex bounds lie in an additive subgroup and every vertex set satisfies both cut inequalities, then some assignment with values in that subgroup has excess within the vertex bounds.

theorem TauCeti.ExcessIntervalFlow.nonempty_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {a b : V → K} (hlo : lo ≤ hi) (hab : a ≤ b) : Nonempty (ExcessIntervalFlow lo hi a b) ↔ (∀ (S : Finset V), ∑ v ∈ S, a v ≤ cutBound lo hi Sᶜ) ∧ ∀ (S : Finset V), -cutBound lo hi S ≤ ∑ v ∈ S, b v

Interval-excess feasibility. For ordered arrow and vertex bounds, an assignment with excess between a and b exists exactly when, for every vertex set S, the lower vertex bounds on S are at most the cut bound of Sᶜ and the upper vertex bounds on S are at least minus the cut bound of S.

theorem TauCeti.ExcessIntervalFlow.exists_mem_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {a b : V → K} (hlo : lo ≤ hi) (hab : a ≤ b) (H : AddSubgroup K) (hloH : ∀ ⦃x y : V⦄ (e : Q x y), lo e ∈ H) (hhiH : ∀ ⦃x y : V⦄ (e : Q x y), hi e ∈ H) (haH : ∀ (v : V), a v ∈ H) (hbH : ∀ (v : V), b v ∈ H) : (∃ (f : ExcessIntervalFlow lo hi a b), ∀ ⦃x y : V⦄ (e : Q x y), ↑f e ∈ H) ↔ (∀ (S : Finset V), ∑ v ∈ S, a v ≤ cutBound lo hi Sᶜ) ∧ ∀ (S : Finset V), -cutBound lo hi S ≤ ∑ v ∈ S, b v

Subgroup-valued interval-excess feasibility has the same cut criterion as unrestricted feasibility when the arrow and vertex bounds take values in the subgroup.

theorem TauCeti.ExcessIntervalFlow.not_nonempty_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {a b : V → K} (hlo : lo ≤ hi) (hab : a ≤ b) : ¬Nonempty (ExcessIntervalFlow lo hi a b) ↔ (∃ (S : Finset V), cutBound lo hi Sᶜ < ∑ v ∈ S, a v) ∨ ∃ (S : Finset V), ∑ v ∈ S, b v < -cutBound lo hi S

An infeasible interval-excess problem has a vertex set strictly violating one of the two cut inequalities. Conversely, either violation rules out every feasible assignment.

theorem TauCeti.ExcessIntervalFlow.nonempty_or_certificate {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {a b : V → K} (hlo : lo ≤ hi) (hab : a ≤ b) : Nonempty (ExcessIntervalFlow lo hi a b) ∨ (∃ (S : Finset V), cutBound lo hi Sᶜ < ∑ v ∈ S, a v) ∨ ∃ (S : Finset V), ∑ v ∈ S, b v < -cutBound lo hi S

Either an interval-excess assignment exists, or a vertex set strictly violates one of the two cut inequalities.

theorem TauCeti.ExcessFlow.nonempty_iff_forall_cutBound {V : Type u} {Q : V → V → Type v} {K : Type w} [Fintype V] [(x y : V) → Fintype (Q x y)] [AddCommGroup K] [LinearOrder K] [IsOrderedAddMonoid K] [DecidableEq V] {lo hi : Assignment Q K} {b : V → K} (hlo : lo ≤ hi) : Nonempty (ExcessFlow lo hi b) ↔ (∀ (S : Finset V), ∑ v ∈ S, b v ≤ cutBound lo hi Sᶜ) ∧ ∀ (S : Finset V), -cutBound lo hi S ≤ ∑ v ∈ S, b v

The interval criterion at equal endpoints characterizes prescribed excess. Taking S = univ in both families recovers the balance condition of ExcessFlow.nonempty_iff.

Empty vertices and signed loops

Flexible supply and demand