OAI/Combinatorics/ContingencyTables/Counting/CompanionInitializedRestartProgram.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Initialization and all stored-multiplier restart stages

Past entries are stored in chronological order. Entry i contains the multiplier for restart phase i+1. Initialization and restart stages take disjoint slices of the supplied word.

  1. abbrev OAI.ContingencyTables.CompanionInitializedRestartProgram.Prepared line 16
  2. abbrev OAI.ContingencyTables.CompanionInitializedRestartProgram.Stored line 17
  3. abbrev OAI.ContingencyTables.CompanionInitializedRestartProgram.Input line 18
  4. def OAI.ContingencyTables.CompanionInitializedRestartProgram.reserve line 20
  5. def OAI.ContingencyTables.CompanionInitializedRestartProgram.reserveRealizer line 21
  6. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.polynomial_reserve line 22
  7. def OAI.ContingencyTables.CompanionInitializedRestartProgram.indices line 25
  8. def OAI.ContingencyTables.CompanionInitializedRestartProgram.indicesRealizer line 26
  9. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.polynomial_indices line 28
  10. def OAI.ContingencyTables.CompanionInitializedRestartProgram.stageAt line 35
  11. def OAI.ContingencyTables.CompanionInitializedRestartProgram.stageAtRealizer line 37
  12. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.polynomial_stageAt line 48
  13. def OAI.ContingencyTables.CompanionInitializedRestartProgram.stages line 59
  14. def OAI.ContingencyTables.CompanionInitializedRestartProgram.stagesRealizer line 61
  15. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.polynomial_stages line 62
  16. def OAI.ContingencyTables.CompanionInitializedRestartProgram.initialWidth line 66
  17. def OAI.ContingencyTables.CompanionInitializedRestartProgram.initialWidthRealizer line 67
  18. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.polynomial_initialWidth line 70
  19. def OAI.ContingencyTables.CompanionInitializedRestartProgram.initialInput line 74
  20. def OAI.ContingencyTables.CompanionInitializedRestartProgram.initialInputRealizer line 76
  21. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.polynomial_initialInput line 80
  22. def OAI.ContingencyTables.CompanionInitializedRestartProgram.initialCode line 84
  23. def OAI.ContingencyTables.CompanionInitializedRestartProgram.initialCodeRealizer line 85
  24. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.polynomial_initialCode line 88
  25. def OAI.ContingencyTables.CompanionInitializedRestartProgram.prepare line 93
  26. def OAI.ContingencyTables.CompanionInitializedRestartProgram.prepareRealizer line 95
  27. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.polynomial_prepare line 99
  28. def OAI.ContingencyTables.CompanionInitializedRestartProgram.output line 103
  29. def OAI.ContingencyTables.CompanionInitializedRestartProgram.outputRealizer line 104
  30. theorem OAI.ContingencyTables.CompanionInitializedRestartProgram.polynomial_output line 107