def NetworkFlow.IsBottleneckEdge {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (p : List V) (hp : IsShortestAugmentingPath N fl p) (u v : V) : Prop

structure NetworkFlow.ShortestAugSeq {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (k : ℕ) : Type u_1

• fl : Fin (k + 1) → STFlow N
• augments (i : Fin k) : IsShortestPathAugmentation N (self.fl i.castSucc) (self.fl i.succ)

noncomputable def NetworkFlow.bottleneckCount {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) {k : ℕ} (seq : ShortestAugSeq N k) (u v : V) : ℕ

theorem NetworkFlow.card_le_of_step_bound {k n : ℕ} (B : Finset (Fin k)) (f : Fin k → ℕ) (hf_ge_one : ∀ i ∈ B, 1 ≤ f i) (hf_bound : ∀ i ∈ B, f i ≤ n - 1) (hf_step : ∀ (i j : Fin k), i ∈ B → j ∈ B → i < j → f i + 2 ≤ f j) : B.card ≤ n / 2

theorem NetworkFlow.dirDist_lt_top_le {V : Type u_1} [Fintype V] [DecidableEq V] (adj : V → V → Prop) (s v : V) (hfin : dirDist adj s v ≠ ⊤) : dirDist adj s v ≤ ↑(Fintype.card V - 1)

theorem NetworkFlow.per_vertex_dist_bound_general {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl' : STFlow N) (p : List V) (hp_aug : IsAugmentingPath N fl p) (hp_shortest : ↑(p.length - 1) = residualDist N fl) (hflow_change : ∀ (u v : V), ¬EdgeOnPath p u v → ¬EdgeOnPath p v u → fl'.f u v = fl.f u v) (v : V) (p' : List V) (hp' : IsDirectedPath (resAdj N fl') N.s v p') (j : ℕ) (hj : 1 ≤ j) (hj2 : j < p'.length) : dirDist (resAdj N fl) N.s (p'.get ⟨j, hj2⟩) ≤ ↑j

theorem NetworkFlow.new_path_length_ge_old_dist_general {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl' : STFlow N) (h : IsShortestPathAugmentation N fl fl') (v : V) (k : ℕ) (p' : List V) (hp' : IsDirectedPath (resAdj N fl') N.s v p') (hlen : p'.length = k + 1) : dirDist (resAdj N fl) N.s v ≤ ↑k

theorem NetworkFlow.vertex_dist_monotone {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl' : STFlow N) (h : IsShortestPathAugmentation N fl fl') (v : V) : dirDist (resAdj N fl) N.s v ≤ dirDist (resAdj N fl') N.s v

theorem NetworkFlow.dist_on_shortest_path {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (p : List V) (hp : IsShortestAugmentingPath N fl p) (u v : V) (huv : EdgeOnPath p u v) (hfin_u : dirDist (resAdj N fl) N.s u ≠ ⊤) : dirDist (resAdj N fl) N.s v = dirDist (resAdj N fl) N.s u + 1

theorem NetworkFlow.dist_finite_on_path {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (p : List V) (hp : IsShortestAugmentingPath N fl p) (u v : V) (huv : EdgeOnPath p u v) (hne : u ≠ N.s) : dirDist (resAdj N fl) N.s u ≠ ⊤

theorem NetworkFlow.vertex_dist_monotone_seq {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) {k : ℕ} (seq : ShortestAugSeq N k) (w : V) (a b : Fin (k + 1)) (hab : a ≤ b) : dirDist (resAdj N (seq.fl a)) N.s w ≤ dirDist (resAdj N (seq.fl b)) N.s w

theorem NetworkFlow.source_not_interior_of_augmenting_path {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (p : List V) (hp : IsAugmentingPath N fl p) (w : V) : ¬EdgeOnPath p w N.s

theorem NetworkFlow.bottleneck_saturated_after_augmentation {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl' : STFlow N) (p : List V) (hp : IsShortestAugmentingPath N fl p) (u v : V) (hbot : IsBottleneckEdge N fl p hp u v) (haug : IsShortestPathAugmentation N fl fl') : ¬resAdj N fl' u v

theorem NetworkFlow.source_edge_bottleneck_at_most_once {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) {k : ℕ} (seq : ShortestAugSeq N k) (v : V) (i j : Fin k) (hij : i < j) (p_i : List V) (hp_i : IsShortestAugmentingPath N (seq.fl i.castSucc) p_i) (hbot_i : IsBottleneckEdge N (seq.fl i.castSucc) p_i hp_i N.s v) (p_j : List V) (hp_j : IsShortestAugmentingPath N (seq.fl j.castSucc) p_j) (hbot_j : IsBottleneckEdge N (seq.fl j.castSucc) p_j hp_j N.s v) : False

theorem NetworkFlow.dist_increase_between_bottlenecks {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) {k : ℕ} (seq : ShortestAugSeq N k) (u v : V) (i j : Fin k) (hij : i < j) (p_i : List V) (hp_i : IsShortestAugmentingPath N (seq.fl i.castSucc) p_i) (hbot_i : IsBottleneckEdge N (seq.fl i.castSucc) p_i hp_i u v) (p_j : List V) (hp_j : IsShortestAugmentingPath N (seq.fl j.castSucc) p_j) (hbot_j : IsBottleneckEdge N (seq.fl j.castSucc) p_j hp_j u v) : dirDist (resAdj N (seq.fl i.castSucc)) N.s u + 2 ≤ dirDist (resAdj N (seq.fl j.castSucc)) N.s u

theorem NetworkFlow.dist_ge_one_of_ne_source {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (p : List V) (hp : IsShortestAugmentingPath N fl p) (u v : V) (huv : EdgeOnPath p u v) (hus : u ≠ N.s) : 1 ≤ dirDist (resAdj N fl) N.s u

theorem NetworkFlow.bottleneck_edge_bound {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) {k : ℕ} (seq : ShortestAugSeq N k) (u v : V) : bottleneckCount N seq u v ≤ Fintype.card V / 2