def NetworkFlow.IsMaxFlow {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : Prop

noncomputable def NetworkFlow.edgeCount {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) : ℕ

theorem NetworkFlow.max_sub_max_neg (a : ℝ) : max a 0 - max (-a) 0 = a

noncomputable def NetworkFlow.residualNetwork {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : FlowNetwork V

noncomputable def NetworkFlow.diffFlowFun {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) (u v : V) : ℝ

theorem NetworkFlow.diffFlowFun_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) (u v : V) : 0 ≤ diffFlowFun N fl fl_max u v

theorem NetworkFlow.diffFlowFun_le_resCap {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) (u v : V) : diffFlowFun N fl fl_max u v ≤ resCap N fl u v

theorem NetworkFlow.diffFlowFun_conservation {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) (w : V) (hw_s : w ≠ N.s) (hw_t : w ≠ N.t) : ∑ u : V, diffFlowFun N fl fl_max u w = ∑ u : V, diffFlowFun N fl fl_max w u

noncomputable def NetworkFlow.diffFlow {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) : STFlow (residualNetwork N fl)

theorem NetworkFlow.diffFlow_value {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) : flowValue (residualNetwork N fl) (diffFlow N fl fl_max) = flowValue N fl_max - flowValue N fl

theorem NetworkFlow.diffFlow_support_le_edgeCount {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) : (flowSupport (residualNetwork N fl) (diffFlow N fl fl_max)).card ≤ edgeCount N

theorem NetworkFlow.flowDecomp_value_eq_sum {V : Type u_1} [Fintype V] [DecidableEq V] {N' : FlowNetwork V} {fl' : STFlow N'} (decomp : FlowDecomposition N' fl') : flowValue N' decomp.f' = ∑ i : Fin decomp.k, decomp.weights i

theorem NetworkFlow.FlowPath.consecutive_mem_edges {V : Type u_1} [Fintype V] [DecidableEq V] {N' : FlowNetwork V} (p : FlowPath N') (idx : ℕ) (hidx : idx + 1 < p.vertices.length) : p.mem_edges p.vertices[idx] p.vertices[idx + 1]

theorem NetworkFlow.FlowDecomposition.sum_ge_weight {V : Type u_1} [Fintype V] [DecidableEq V] {N' : FlowNetwork V} {fl' : STFlow N'} (decomp : FlowDecomposition N' fl') (i : Fin decomp.k) (u v : V) (hmem : (decomp.paths i).mem_edges u v) : decomp.weights i ≤ ∑ j : Fin decomp.k, if (decomp.paths j).mem_edges u v then decomp.weights j else 0

theorem NetworkFlow.flowPath_to_augmenting {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) (decomp : FlowDecomposition (residualNetwork N fl) (diffFlow N fl fl_max)) (i : Fin decomp.k) : IsAugmentingPath N fl (decomp.paths i).vertices

theorem NetworkFlow.residual_decomposition_exists {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) (hlt : flowValue N fl < flowValue N fl_max) (m : ℕ) (hm : m = edgeCount N) (hm_pos : 0 < m) : ∃ (k : ℕ) (paths : Fin k → List V) (hp_aug : ∀ (i : Fin k), IsAugmentingPath N fl (paths i)) (weights : Fin k → ℝ), 0 < k ∧ k ≤ m ∧ (∀ (i : Fin k), 0 < weights i) ∧ ∑ i : Fin k, weights i = flowValue N fl_max - flowValue N fl ∧ ∀ (i : Fin k), weights i ≤ pathBottleneck N fl (paths i) ⋯

theorem NetworkFlow.large_augmenting_path {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl_max : STFlow N) (hmax : IsMaxFlow N fl_max) (hlt : flowValue N fl < flowValue N fl_max) (m : ℕ) (hm : m = edgeCount N) (hm_pos : 0 < m) : ∃ (p : List V) (hp : IsAugmentingPath N fl p), pathBottleneck N fl p ⋯ ≥ (flowValue N fl_max - flowValue N fl) / ↑m