OAI/Combinatorics/ContingencyTables/Transport/LayeredTableNetwork.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

The source-row-column-sink network for bounded tables

The only nonzero capacities are the three layers prescribed in the manuscript. Both antiparallel orientations are stored as one skew flow.

  1. abbrev OAI.ContingencyTables.LayeredTableNetwork.Vertex line 18
  2. def OAI.ContingencyTables.LayeredTableNetwork.source line 22
  3. def OAI.ContingencyTables.LayeredTableNetwork.sink line 23
  4. def OAI.ContingencyTables.LayeredTableNetwork.row line 24
  5. def OAI.ContingencyTables.LayeredTableNetwork.column line 25
  6. def OAI.ContingencyTables.LayeredTableNetwork.capacity line 27
  7. def OAI.ContingencyTables.LayeredTableNetwork.Feasible line 34
  8. def OAI.ContingencyTables.LayeredTableNetwork.value line 40
  9. def OAI.ContingencyTables.LayeredTableNetwork.tableFlow line 42
  10. lemma OAI.ContingencyTables.LayeredTableNetwork.capacity_diagonal line 52
  11. lemma OAI.ContingencyTables.LayeredTableNetwork.tableFlow_skew line 59
  12. theorem OAI.ContingencyTables.LayeredTableNetwork.tableFlow_feasible line 64
  13. theorem OAI.ContingencyTables.LayeredTableNetwork.tableFlow_value line 80
  14. lemma OAI.ContingencyTables.LayeredTableNetwork.zero_of_no_capacity line 84
  15. lemma OAI.ContingencyTables.LayeredTableNetwork.row_column_nonnegative line 95
  16. lemma OAI.ContingencyTables.LayeredTableNetwork.source_value line 103
  17. theorem OAI.ContingencyTables.LayeredTableNetwork.value_le_total line 113
  18. lemma OAI.ContingencyTables.LayeredTableNetwork.row_balance line 119
  19. lemma OAI.ContingencyTables.LayeredTableNetwork.column_balance line 134
  20. lemma OAI.ContingencyTables.LayeredTableNetwork.saturation line 150
  21. lemma OAI.ContingencyTables.LayeredTableNetwork.source_saturated line 160
  22. lemma OAI.ContingencyTables.LayeredTableNetwork.column_saturated line 169
  23. def OAI.ContingencyTables.LayeredTableNetwork.decode line 189
  24. theorem OAI.ContingencyTables.LayeredTableNetwork.decode_boundedTable line 192