OAI/Combinatorics/ContingencyTables/Counting/CompanionRestartProgram.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Executed restart stages with disjoint variable-width words

The supplied stage list determines the number of iterations. The current encoded profile is bounded by the original profile length after every stage.

  1. abbrev OAI.ContingencyTables.CompanionRestartProgram.Stage line 15
  2. abbrev OAI.ContingencyTables.CompanionRestartProgram.Input line 16
  3. abbrev OAI.ContingencyTables.CompanionRestartProgram.State line 17
  4. def OAI.ContingencyTables.CompanionRestartProgram.request line 19
  5. def OAI.ContingencyTables.CompanionRestartProgram.requestRealizer line 21
  6. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_request line 26
  7. def OAI.ContingencyTables.CompanionRestartProgram.indices line 32
  8. def OAI.ContingencyTables.CompanionRestartProgram.indicesRealizer line 33
  9. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_indices line 35
  10. def OAI.ContingencyTables.CompanionRestartProgram.indexedWidth line 43
  11. def OAI.ContingencyTables.CompanionRestartProgram.indexedWidthRealizer line 44
  12. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_indexedWidth line 47
  13. def OAI.ContingencyTables.CompanionRestartProgram.widths line 50
  14. def OAI.ContingencyTables.CompanionRestartProgram.widthsRealizer line 51
  15. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_widths line 53
  16. def OAI.ContingencyTables.CompanionRestartProgram.stageWord line 57
  17. def OAI.ContingencyTables.CompanionRestartProgram.stageWordRealizer line 58
  18. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_stageWord line 63
  19. def OAI.ContingencyTables.CompanionRestartProgram.stageInput line 69
  20. def OAI.ContingencyTables.CompanionRestartProgram.stageInputRealizer line 71
  21. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_stageInput line 79
  22. def OAI.ContingencyTables.CompanionRestartProgram.candidate line 91
  23. def OAI.ContingencyTables.CompanionRestartProgram.candidateRealizer line 92
  24. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_candidate line 95
  25. def OAI.ContingencyTables.CompanionRestartProgram.bound line 98
  26. def OAI.ContingencyTables.CompanionRestartProgram.boundRealizer line 99
  27. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_bound line 101
  28. def OAI.ContingencyTables.CompanionRestartProgram.next line 108
  29. def OAI.ContingencyTables.CompanionRestartProgram.nextRealizer line 109
  30. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_next line 112
  31. def OAI.ContingencyTables.CompanionRestartProgram.advance line 116
  32. def OAI.ContingencyTables.CompanionRestartProgram.advanceRealizer line 117
  33. lemma OAI.ContingencyTables.CompanionRestartProgram.polynomial_advance line 118
  34. lemma OAI.ContingencyTables.CompanionRestartProgram.advance_weight line 121
  35. def OAI.ContingencyTables.CompanionRestartProgram.walk line 132
  36. def OAI.ContingencyTables.CompanionRestartProgram.walkRealizer line 133
  37. lemma OAI.ContingencyTables.CompanionRestartProgram.fold_fixed line 135
  38. lemma OAI.ContingencyTables.CompanionRestartProgram.fold_weight line 141
  39. theorem OAI.ContingencyTables.CompanionRestartProgram.polynomial_walk line 152
  40. def OAI.ContingencyTables.CompanionRestartProgram.output line 159
  41. def OAI.ContingencyTables.CompanionRestartProgram.outputRealizer line 160
  42. theorem OAI.ContingencyTables.CompanionRestartProgram.polynomial_output line 165