OAI/Combinatorics/ContingencyTables/Machines/FlowMatrixProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Materialized binary residual augmentation

The path and bottleneck are computed once, then every matrix entry is updated from the preceding matrix. Missing paths leave that matrix unchanged.

  1. def OAI.ContingencyTables.FlowMatrixProgram.updateRow line 18
  2. def OAI.ContingencyTables.FlowMatrixProgram.updateRowRealizer line 21
  3. lemma OAI.ContingencyTables.FlowMatrixProgram.polynomial_updateRow line 32
  4. def OAI.ContingencyTables.FlowMatrixProgram.updateMatrix line 42
  5. def OAI.ContingencyTables.FlowMatrixProgram.updateMatrixRealizer line 45
  6. lemma OAI.ContingencyTables.FlowMatrixProgram.polynomial_updateMatrix line 52
  7. lemma OAI.ContingencyTables.FlowMatrixProgram.updateMatrix_code line 57
  8. def OAI.ContingencyTables.FlowMatrixProgram.prepareAugment line 72
  9. def OAI.ContingencyTables.FlowMatrixProgram.prepareAugmentRealizer line 75
  10. lemma OAI.ContingencyTables.FlowMatrixProgram.polynomial_prepareAugment line 78
  11. def OAI.ContingencyTables.FlowMatrixProgram.augment line 82
  12. def OAI.ContingencyTables.FlowMatrixProgram.augmentRealizer line 84
  13. lemma OAI.ContingencyTables.FlowMatrixProgram.polynomial_augment line 87
  14. def OAI.ContingencyTables.FlowMatrixProgram.advance line 90
  15. def OAI.ContingencyTables.FlowMatrixProgram.advanceRealizer line 95
  16. lemma OAI.ContingencyTables.FlowMatrixProgram.polynomial_advance line 103
  17. lemma OAI.ContingencyTables.FlowMatrixProgram.search_residual_nonnegative line 111
  18. theorem OAI.ContingencyTables.FlowMatrixProgram.advance_code line 121