OAI/Combinatorics/ContingencyTables/Counting/CompanionOuterPhaseProgram.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

One complete adaptive phase from the stored chronological history

  1. abbrev OAI.ContingencyTables.CompanionOuterPhaseProgram.Prepared line 10
  2. abbrev OAI.ContingencyTables.CompanionOuterPhaseProgram.Stored line 11
  3. abbrev OAI.ContingencyTables.CompanionOuterPhaseProgram.Request line 12
  4. abbrev OAI.ContingencyTables.CompanionOuterPhaseProgram.Input line 13
  5. def OAI.ContingencyTables.CompanionOuterPhaseProgram.history line 22
  6. def OAI.ContingencyTables.CompanionOuterPhaseProgram.historyRealizer line 23
  7. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_history line 24
  8. def OAI.ContingencyTables.CompanionOuterPhaseProgram.phase line 27
  9. def OAI.ContingencyTables.CompanionOuterPhaseProgram.phaseRealizer line 28
  10. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_phase line 30
  11. def OAI.ContingencyTables.CompanionOuterPhaseProgram.old line 33
  12. def OAI.ContingencyTables.CompanionOuterPhaseProgram.oldRealizer line 35
  13. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_old line 40
  14. def OAI.ContingencyTables.CompanionOuterPhaseProgram.reserve line 50
  15. def OAI.ContingencyTables.CompanionOuterPhaseProgram.reserveRealizer line 51
  16. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_reserve line 52
  17. def OAI.ContingencyTables.CompanionOuterPhaseProgram.contextInput line 55
  18. def OAI.ContingencyTables.CompanionOuterPhaseProgram.contextInputRealizer line 57
  19. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_contextInput line 61
  20. def OAI.ContingencyTables.CompanionOuterPhaseProgram.configAt line 68
  21. def OAI.ContingencyTables.CompanionOuterPhaseProgram.configAtRealizer line 70
  22. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_configAt line 74
  23. def OAI.ContingencyTables.CompanionOuterPhaseProgram.restartRequest line 78
  24. def OAI.ContingencyTables.CompanionOuterPhaseProgram.restartRequestRealizer line 79
  25. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_restartRequest line 81
  26. def OAI.ContingencyTables.CompanionOuterPhaseProgram.restartWidth line 85
  27. def OAI.ContingencyTables.CompanionOuterPhaseProgram.restartWidthRealizer line 86
  28. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_restartWidth line 89
  29. def OAI.ContingencyTables.CompanionOuterPhaseProgram.restartInput line 92
  30. def OAI.ContingencyTables.CompanionOuterPhaseProgram.restartInputRealizer line 94
  31. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_restartInput line 96
  32. def OAI.ContingencyTables.CompanionOuterPhaseProgram.startCode line 99
  33. def OAI.ContingencyTables.CompanionOuterPhaseProgram.startCodeRealizer line 100
  34. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_startCode line 103
  35. def OAI.ContingencyTables.CompanionOuterPhaseProgram.parameters line 106
  36. def OAI.ContingencyTables.CompanionOuterPhaseProgram.parametersRealizer line 107
  37. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_parameters line 108
  38. def OAI.ContingencyTables.CompanionOuterPhaseProgram.precision line 112
  39. def OAI.ContingencyTables.CompanionOuterPhaseProgram.precisionRealizer line 113
  40. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_precision line 116
  41. def OAI.ContingencyTables.CompanionOuterPhaseProgram.observations line 119
  42. def OAI.ContingencyTables.CompanionOuterPhaseProgram.observationsRealizer line 120
  43. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_observations line 123
  44. def OAI.ContingencyTables.CompanionOuterPhaseProgram.walkState line 128
  45. def OAI.ContingencyTables.CompanionOuterPhaseProgram.walkStateRealizer line 130
  46. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_walkState line 133
  47. def OAI.ContingencyTables.CompanionOuterPhaseProgram.widthInput line 138
  48. def OAI.ContingencyTables.CompanionOuterPhaseProgram.widthInputRealizer line 140
  49. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_widthInput line 143
  50. def OAI.ContingencyTables.CompanionOuterPhaseProgram.trajectoryWidth line 148
  51. def OAI.ContingencyTables.CompanionOuterPhaseProgram.trajectoryWidthRealizer line 149
  52. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_trajectoryWidth line 152
  53. def OAI.ContingencyTables.CompanionOuterPhaseProgram.afterRestart line 156
  54. def OAI.ContingencyTables.CompanionOuterPhaseProgram.afterRestartRealizer line 157
  55. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_afterRestart line 158
  56. def OAI.ContingencyTables.CompanionOuterPhaseProgram.trajectoryInput line 161
  57. def OAI.ContingencyTables.CompanionOuterPhaseProgram.trajectoryInputRealizer line 163
  58. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_trajectoryInput line 166
  59. def OAI.ContingencyTables.CompanionOuterPhaseProgram.trialInput line 170
  60. def OAI.ContingencyTables.CompanionOuterPhaseProgram.trialInputRealizer line 172
  61. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_trialInput line 175
  62. def OAI.ContingencyTables.CompanionOuterPhaseProgram.fallback line 182
  63. def OAI.ContingencyTables.CompanionOuterPhaseProgram.fallbackRealizer line 183
  64. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_fallback line 185
  65. def OAI.ContingencyTables.CompanionOuterPhaseProgram.output line 190
  66. def OAI.ContingencyTables.CompanionOuterPhaseProgram.outputRealizer line 191
  67. lemma OAI.ContingencyTables.CompanionOuterPhaseProgram.polynomial_output line 196