OAI/Combinatorics/ContingencyTables/Machines/FlowLoopProgram.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Polynomial binary execution of the bounded residual-flow loop

  1. abbrev OAI.ContingencyTables.FlowLoopProgram.Context line 11
  2. abbrev OAI.ContingencyTables.FlowLoopProgram.State line 12
  3. def OAI.ContingencyTables.FlowLoopProgram.step line 14
  4. def OAI.ContingencyTables.FlowLoopProgram.stepRealizer line 17
  5. lemma OAI.ContingencyTables.FlowLoopProgram.polynomial_step line 23
  6. lemma OAI.ContingencyTables.FlowLoopProgram.fold_context line 31
  7. lemma OAI.ContingencyTables.FlowLoopProgram.fold_weight line 37
  8. theorem OAI.ContingencyTables.FlowLoopProgram.polynomial_loop line 47
  9. def OAI.ContingencyTables.FlowLoopProgram.zeroMatrix line 69
  10. def OAI.ContingencyTables.FlowLoopProgram.zeroMatrixRealizer line 72
  11. lemma OAI.ContingencyTables.FlowLoopProgram.polynomial_zeroMatrix line 74
  12. lemma OAI.ContingencyTables.FlowLoopProgram.zeroMatrix_code line 77
  13. def OAI.ContingencyTables.FlowLoopProgram.cube line 82
  14. def OAI.ContingencyTables.FlowLoopProgram.cubeRealizer line 84
  15. lemma OAI.ContingencyTables.FlowLoopProgram.polynomial_cube line 87
  16. def OAI.ContingencyTables.FlowLoopProgram.iterationCount line 92
  17. def OAI.ContingencyTables.FlowLoopProgram.iterationCountRealizer line 94
  18. lemma OAI.ContingencyTables.FlowLoopProgram.polynomial_iterationCount line 97
  19. def OAI.ContingencyTables.FlowLoopProgram.steps line 101
  20. def OAI.ContingencyTables.FlowLoopProgram.stepsRealizer line 103
  21. lemma OAI.ContingencyTables.FlowLoopProgram.polynomial_steps line 105
  22. def OAI.ContingencyTables.FlowLoopProgram.prepare line 112
  23. def OAI.ContingencyTables.FlowLoopProgram.prepareRealizer line 114
  24. lemma OAI.ContingencyTables.FlowLoopProgram.polynomial_prepare line 119
  25. def OAI.ContingencyTables.FlowLoopProgram.run line 127
  26. def OAI.ContingencyTables.FlowLoopProgram.runRealizer line 130
  27. theorem OAI.ContingencyTables.FlowLoopProgram.polynomial_run line 133
  28. lemma OAI.ContingencyTables.FlowLoopProgram.step_code line 137
  29. lemma OAI.ContingencyTables.FlowLoopProgram.fold_code line 147
  30. theorem OAI.ContingencyTables.FlowLoopProgram.run_code line 158
  31. theorem OAI.ContingencyTables.FlowLoopProgram.run_maximum line 169