OAI/Combinatorics/ContingencyTables/Transport/EdmondsKarpAlgorithm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The bounded deterministic integral max-flow algorithm

Conditional on the augmentation-count bound, concrete residual searches, bottlenecks and flow updates preserve feasibility and yield a stopping certificate.

  1. def OAI.ContingencyTables.EdmondsKarpAlgorithm.advance line 19
  2. def OAI.ContingencyTables.EdmondsKarpAlgorithm.run line 22
  3. def OAI.ContingencyTables.EdmondsKarpAlgorithm.maxFlow line 26
  4. lemma OAI.ContingencyTables.EdmondsKarpAlgorithm.zero_feasible line 28
  5. lemma OAI.ContingencyTables.EdmondsKarpAlgorithm.run_feasible line 36
  6. lemma OAI.ContingencyTables.EdmondsKarpAlgorithm.run_step line 47
  7. lemma OAI.ContingencyTables.EdmondsKarpAlgorithm.run_stops line 51
  8. theorem OAI.ContingencyTables.EdmondsKarpAlgorithm.termination line 59
  9. theorem OAI.ContingencyTables.EdmondsKarpAlgorithm.maxFlow_correct line 80