OAI/Combinatorics/ContingencyTables/Machines/NetworkCapacityProgram.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Constructing the bounded-table capacity network in binary

  1. abbrev OAI.ContingencyTables.NetworkCapacityProgram.EntryInput line 12
  2. def OAI.ContingencyTables.NetworkCapacityProgram.kindRealizer line 14
  3. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_kind line 22
  4. def OAI.ContingencyTables.NetworkCapacityProgram.rowCount line 35
  5. def OAI.ContingencyTables.NetworkCapacityProgram.rowCountRealizer line 37
  6. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_rowCount line 40
  7. def OAI.ContingencyTables.NetworkCapacityProgram.columnBase line 45
  8. def OAI.ContingencyTables.NetworkCapacityProgram.columnBaseRealizer line 47
  9. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_columnBase line 51
  10. def OAI.ContingencyTables.NetworkCapacityProgram.kinds line 55
  11. def OAI.ContingencyTables.NetworkCapacityProgram.kindsRealizer line 58
  12. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_kinds line 62
  13. def OAI.ContingencyTables.NetworkCapacityProgram.pattern line 68
  14. def OAI.ContingencyTables.NetworkCapacityProgram.patternRealizer line 71
  15. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_pattern line 76
  16. def OAI.ContingencyTables.NetworkCapacityProgram.rowRead line 84
  17. def OAI.ContingencyTables.NetworkCapacityProgram.rowReadRealizer line 86
  18. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_rowRead line 90
  19. def OAI.ContingencyTables.NetworkCapacityProgram.columnRead line 98
  20. def OAI.ContingencyTables.NetworkCapacityProgram.columnReadRealizer line 100
  21. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_columnRead line 104
  22. def OAI.ContingencyTables.NetworkCapacityProgram.boundRead line 112
  23. def OAI.ContingencyTables.NetworkCapacityProgram.boundReadRealizer line 115
  24. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_boundRead line 121
  25. def OAI.ContingencyTables.NetworkCapacityProgram.entryRealizer line 132
  26. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_entry line 149
  27. def OAI.ContingencyTables.NetworkCapacityProgram.vertexCountRealizer line 154
  28. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_vertexCount line 163
  29. def OAI.ContingencyTables.NetworkCapacityProgram.vertices line 171
  30. def OAI.ContingencyTables.NetworkCapacityProgram.verticesRealizer line 172
  31. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_vertices line 174
  32. def OAI.ContingencyTables.NetworkCapacityProgram.row line 182
  33. def OAI.ContingencyTables.NetworkCapacityProgram.rowRealizer line 185
  34. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_row line 190
  35. def OAI.ContingencyTables.NetworkCapacityProgram.matrixRealizer line 198
  36. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_matrix line 201
  37. def OAI.ContingencyTables.NetworkCapacityProgram.solve line 205
  38. def OAI.ContingencyTables.NetworkCapacityProgram.solveRealizer line 207
  39. lemma OAI.ContingencyTables.NetworkCapacityProgram.polynomial_solve line 210
  40. theorem OAI.ContingencyTables.NetworkCapacityProgram.solve_code line 214