OAI/Combinatorics/ContingencyTables/Transport/EdmondsKarpTrace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.EdmondsKarpTrace.descent_between line 13
2. lemma OAI.ContingencyTables.EdmondsKarpTrace.labels_monotone line 41
3. theorem OAI.ContingencyTables.EdmondsKarpTrace.repeated_critical line 50

   Source documentation

   Once (u,v) is saturated, using it again requires a reverse augmentation and hence at least two more source-distance layers at u.

   theorem repeated_critical {c : Capacity n} {s t : Fin n} {F : Fin (K+1)→Flow n}
       (h : ∀ i : Fin K,ShortestAugmentation c s t (F i.castSucc) (F i.succ))
       (i j : Fin K) (hij : i < j) (u v : Fin n)
       (hsat : F i.succ u v=(c u v:ℤ))
       (hlevel : label c (F i.castSucc) s v=label c (F i.castSucc) s u+1)
       (hres : F j.castSucc u v < (c u v:ℤ)) :
       label c (F i.castSucc) s u+2 ≤ label c (F j.castSucc) s u := by
   …