EdmondsKarpAugmentation.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Label monotonicity and critical arcs of a shortest augmentation

lemma OAI.ContingencyTables.EdmondsKarpAugmentation.reverse_count_zero line 13
lemma OAI.ContingencyTables.EdmondsKarpAugmentation.update_decrease line 22
lemma OAI.ContingencyTables.EdmondsKarpAugmentation.update_new_edge line 32
lemma OAI.ContingencyTables.EdmondsKarpAugmentation.update_saturates line 40
theorem OAI.ContingencyTables.EdmondsKarpAugmentation.labels_monotone line 49
Source documentation
All old distance labels remain valid lower potentials for the new residual graph, including arcs created by cancellation of flow.
```
theorem labels_monotone {c : Capacity n} {s t : Fin n} {f g : Flow n}
    (h : ShortestAugmentation c s t f g) (v : Fin n) : label c f s v ≤ label c g s v := by
…
```
theorem OAI.ContingencyTables.EdmondsKarpAugmentation.decrease_labels line 69
Source documentation
A decrease of flow on (u,v) means the augmentation used (v,u). Consequently u was one distance layer beyond v.
```
theorem decrease_labels {c : Capacity n} {s t : Fin n} {f g : Flow n}
    (h : ShortestAugmentation c s t f g) (u v : Fin n) (hdec : g u v < f u v) :
    label c f s u=label c f s v+1 := by
…
```

theorem OAI.ContingencyTables.EdmondsKarpAugmentation.critical_arc line 85

Source documentation

Each augmentation has an arc which was residual, becomes saturated, and points from one finite distance layer to the next.

theorem critical_arc {c : Capacity n} {s t : Fin n} {f g : Flow n}
    (h : ShortestAugmentation c s t f g) :
    ∃ u v : Fin n,f u v < (c u v:ℤ) ∧ g u v=(c u v:ℤ) ∧
      label c f s v=label c f s u+1 ∧ label c f s u < n := by
…