OAI/Combinatorics/ContingencyTables/Transport/BoundedTableFeasibility.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Executed bounded-table feasibility from the cited flow bound

The test runs the concrete residual algorithm on the literal three-layer network. It handles zero margins, empty row or column types, and structural zeros. No bounded-table feasibility oracle is assumed.

  1. def OAI.ContingencyTables.BoundedTableFeasibility.vertices line 18
  2. def OAI.ContingencyTables.BoundedTableFeasibility.networkCapacity line 23
  3. def OAI.ContingencyTables.BoundedTableFeasibility.pull line 27
  4. def OAI.ContingencyTables.BoundedTableFeasibility.push line 30
  5. lemma OAI.ContingencyTables.BoundedTableFeasibility.source_ne_sink line 33
  6. lemma OAI.ContingencyTables.BoundedTableFeasibility.capacity_loop line 38
  7. lemma OAI.ContingencyTables.BoundedTableFeasibility.pull_feasible line 42
  8. lemma OAI.ContingencyTables.BoundedTableFeasibility.push_feasible line 56
  9. lemma OAI.ContingencyTables.BoundedTableFeasibility.pull_value line 67
  10. lemma OAI.ContingencyTables.BoundedTableFeasibility.push_value line 71
  11. def OAI.ContingencyTables.BoundedTableFeasibility.computedFlow line 76
  12. def OAI.ContingencyTables.BoundedTableFeasibility.feasibleTest line 81
  13. theorem OAI.ContingencyTables.BoundedTableFeasibility.computedFlow_feasible line 84
  14. theorem OAI.ContingencyTables.BoundedTableFeasibility.feasibleTest_correct line 90