OAI/Combinatorics/ContingencyTables/Machines/ResidualGraphProgram.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Binary construction and search of the actual residual graph

  1. abbrev OAI.ContingencyTables.ResidualGraphProgram.NatMatrix line 13
  2. abbrev OAI.ContingencyTables.ResidualGraphProgram.FlowMatrix line 14
  3. abbrev OAI.ContingencyTables.ResidualGraphProgram.Data line 15
  4. abbrev OAI.ContingencyTables.ResidualGraphProgram.ArcInput line 16
  5. def OAI.ContingencyTables.ResidualGraphProgram.matrixIndices line 18
  6. def OAI.ContingencyTables.ResidualGraphProgram.matrixIndicesRealizer line 20
  7. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_matrixIndices line 22
  8. def OAI.ContingencyTables.ResidualGraphProgram.capacityEntry line 27
  9. def OAI.ContingencyTables.ResidualGraphProgram.capacityEntryRealizer line 30
  10. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_capacityEntry line 34
  11. def OAI.ContingencyTables.ResidualGraphProgram.flowEntry line 40
  12. def OAI.ContingencyTables.ResidualGraphProgram.flowEntryRealizer line 43
  13. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_flowEntry line 47
  14. def OAI.ContingencyTables.ResidualGraphProgram.arcData line 53
  15. def OAI.ContingencyTables.ResidualGraphProgram.arcDataRealizer line 56
  16. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_arcData line 60
  17. def OAI.ContingencyTables.ResidualGraphProgram.residualValue line 68
  18. def OAI.ContingencyTables.ResidualGraphProgram.residualValueRealizer line 70
  19. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_residualValue line 74
  20. def OAI.ContingencyTables.ResidualGraphProgram.positive line 79
  21. def OAI.ContingencyTables.ResidualGraphProgram.positiveRealizer line 81
  22. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_positive line 85
  23. def OAI.ContingencyTables.ResidualGraphProgram.arc line 91
  24. def OAI.ContingencyTables.ResidualGraphProgram.arcRealizer line 92
  25. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_arc line 93
  26. def OAI.ContingencyTables.ResidualGraphProgram.arcRow line 96
  27. def OAI.ContingencyTables.ResidualGraphProgram.arcRowRealizer line 99
  28. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_arcRow line 110
  29. def OAI.ContingencyTables.ResidualGraphProgram.graph line 119
  30. def OAI.ContingencyTables.ResidualGraphProgram.graphRealizer line 122
  31. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_graph line 129
  32. def OAI.ContingencyTables.ResidualGraphProgram.natCode line 134
  33. def OAI.ContingencyTables.ResidualGraphProgram.flowCode line 137
  34. lemma OAI.ContingencyTables.ResidualGraphProgram.capacityEntry_code line 140
  35. lemma OAI.ContingencyTables.ResidualGraphProgram.flowEntry_code line 145
  36. lemma OAI.ContingencyTables.ResidualGraphProgram.residualValue_correct line 150
  37. lemma OAI.ContingencyTables.ResidualGraphProgram.positive_correct line 156
  38. lemma OAI.ContingencyTables.ResidualGraphProgram.arc_code line 165
  39. lemma OAI.ContingencyTables.ResidualGraphProgram.graph_code line 171
  40. def OAI.ContingencyTables.ResidualGraphProgram.search line 182
  41. def OAI.ContingencyTables.ResidualGraphProgram.searchRealizer line 185
  42. lemma OAI.ContingencyTables.ResidualGraphProgram.polynomial_search line 189
  43. lemma OAI.ContingencyTables.ResidualGraphProgram.search_code line 196