Distances along arrows of positive capacity

For capacities c on an arrow family Q, the positive distance positiveEDist c s t is the least length of a walk from s to t that traverses only arrows of positive capacity, and ⊤ when there is no such walk. For the residual capacities of a flow it is the length of a shortest augmenting walk, the quantity that controls shortest-path augmentation. The definition follows Mathlib's SimpleGraph.edist, the infimum in ℕ∞ of the lengths of walks.

Along every arrow of positive capacity the distance from s rises by at most one, and conversely every function vanishing at s with this property is a lower bound for the distance from s. Along a shortest walk the distance rises by exactly one at every arrow, so a shortest walk is a path, and a finite positive distance is less than the number of vertices.

Main definitions

• TauCeti.positiveEDist c s t: the positive distance from s to t for the capacities c.

Main results

• TauCeti.positiveEDist_ne_top_iff: the positive distance is finite exactly for positively reachable vertices, and TauCeti.PositiveReachable.exists_length_eq_positiveEDist gives a walk attaining it.
• TauCeti.positiveEDist_le_add_one and TauCeti.le_positiveEDist: the positive distance from s is the largest function vanishing at s that rises by at most one along every arrow of positive capacity.
• TauCeti.positiveEDist_eq_add_one_of_mem_arrows and TauCeti.positiveEDist_lt_of_mem_arrows: every arrow of a shortest walk raises the distance by one.
• TauCeti.ArrowWalk.isPath_of_length_eq_positiveEDist: a shortest walk is a path.
• TauCeti.positiveEDist_lt_card: finite positive distances are less than the number of vertices.

noncomputable def TauCeti.positiveEDist {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] (c : Assignment Q K) (s t : V) : ℕ∞

The positive distance from s to t for the capacities c: the least length of a walk from s to t that traverses only arrows of positive capacity, or ⊤ if t is not positively reachable from s. For residual capacities it is the length of a shortest augmenting walk.

theorem TauCeti.positiveEDist_def {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} : positiveEDist c s t = ⨅ (p : { p : ArrowWalk Q s t // ∀ a ∈ p.arrows, 0 < c a.snd.snd }), ↑(↑p).length

theorem TauCeti.positiveEDist_le_length {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} (p : ArrowWalk Q s t) (hp : ∀ a ∈ p.arrows, 0 < c a.snd.snd) : positiveEDist c s t ≤ ↑p.length

@[simp]

theorem TauCeti.positiveEDist_self {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] (c : Assignment Q K) (s : V) : positiveEDist c s s = 0

theorem TauCeti.positiveEDist_ne_top_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} : positiveEDist c s t ≠ ⊤ ↔ PositiveReachable c s t

theorem TauCeti.positiveEDist_eq_top_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} : positiveEDist c s t = ⊤ ↔ ¬PositiveReachable c s t

theorem TauCeti.PositiveReachable.exists_length_eq_positiveEDist {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} (h : PositiveReachable c s t) : ∃ (p : ArrowWalk Q s t), (∀ a ∈ p.arrows, 0 < c a.snd.snd) ∧ ↑p.length = positiveEDist c s t

A positively reachable vertex is reached by a walk of shortest length along arrows of positive capacity.

@[simp]

theorem TauCeti.positiveEDist_eq_zero_iff {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} : positiveEDist c s t = 0 ↔ s = t

theorem TauCeti.positiveEDist_le_add_one {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t x : V} (e : Q t x) (he : 0 < c e) : positiveEDist c s x ≤ positiveEDist c s t + 1

Following an arrow of positive capacity raises the positive distance by at most one.

theorem TauCeti.le_positiveEDist {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s : V} {φ : V → ℕ∞} (hs : φ s = 0) (h : ∀ ⦃u v : V⦄ (e : Q u v), 0 < c e → φ v ≤ φ u + 1) (t : V) : φ t ≤ positiveEDist c s t

A lower bound for positive distances: a function vanishing at s that rises by at most one along every arrow of positive capacity is at most the positive distance from s.

theorem TauCeti.positiveEDist_eq_add_one_of_mem_arrows {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} {p : ArrowWalk Q s t} (hp : ∀ a ∈ p.arrows, 0 < c a.snd.snd) (hlen : ↑p.length = positiveEDist c s t) {a : (x : V) × (y : V) × Q x y} (ha : a ∈ p.arrows) : positiveEDist c s a.snd.fst = positiveEDist c s a.fst + 1

Shortest walks. Every arrow of a shortest walk along arrows of positive capacity from s raises the positive distance from s by one.

theorem TauCeti.positiveEDist_lt_of_mem_arrows {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} {p : ArrowWalk Q s t} (hp : ∀ a ∈ p.arrows, 0 < c a.snd.snd) (hlen : ↑p.length = positiveEDist c s t) {a : (x : V) × (y : V) × Q x y} (ha : a ∈ p.arrows) : positiveEDist c s a.fst < positiveEDist c s a.snd.fst

The positive distance from s strictly increases along every arrow of a shortest walk along arrows of positive capacity from s.

theorem TauCeti.ArrowWalk.isPath_of_length_eq_positiveEDist {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} {p : ArrowWalk Q s t} (hp : ∀ a ∈ p.arrows, 0 < c a.snd.snd) (hlen : ↑p.length = positiveEDist c s t) : p.IsPath

A shortest walk along arrows of positive capacity is a path.

theorem TauCeti.positiveEDist_lt_card {V : Type u} {Q : V → V → Type v} {K : Type w} [Zero K] [LT K] {c : Assignment Q K} {s t : V} [Fintype V] (h : PositiveReachable c s t) : positiveEDist c s t < ↑(Fintype.card V)

A positively reachable vertex is at positive distance less than the number of vertices.