OAI/Combinatorics/ContingencyTables/Rooted/RootedEstimatorLayoutProgram.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Computed sizes of the estimator's disjoint word banks

The schedule supplies the phase and sample counts and the two walk times. The catalog itself supplies both the integer-draw widths and the initial free-assignment count. No list is allocated from a binary count here.

  1. abbrev OAI.ContingencyTables.RootedEstimatorLayoutProgram.State line 16
  2. abbrev OAI.ContingencyTables.RootedEstimatorLayoutProgram.Schedule line 17
  3. abbrev OAI.ContingencyTables.RootedEstimatorLayoutProgram.Context line 18
  4. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.stepWidth line 20
  5. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.stepWidthRealizer line 21
  6. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_stepWidth line 24
  7. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.ratioWidth line 28
  8. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.ratioWidthRealizer line 29
  9. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_ratioWidth line 34
  10. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.ratioBlockWidth line 40
  11. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.ratioBlockWidthRealizer line 41
  12. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_ratioBlockWidth line 45
  13. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.ratioBankWidth line 50
  14. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.ratioBankWidthRealizer line 51
  15. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_ratioBankWidth line 55
  16. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.binFrame line 60
  17. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.binFrameRealizer line 62
  18. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_binFrame line 70
  19. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.frames line 86
  20. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.framesRealizer line 87
  21. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_frames line 90
  22. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.binWidth line 95
  23. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.binWidthRealizer line 96
  24. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_binWidth line 100
  25. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.assignmentCount line 104
  26. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.rangeValue line 105
  27. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.rangeValueRealizer line 106
  28. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_rangeValue line 107
  29. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.rangeValues line 110
  30. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.rangeValuesRealizer line 111
  31. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_rangeValues line 112
  32. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.assignmentCountRealizer line 116
  33. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_assignmentCount line 124
  34. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.correctionWalkWidth line 130
  35. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.correctionWalkWidthRealizer line 131
  36. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_correctionWalkWidth line 136
  37. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.correctionWidth line 142
  38. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.correctionWidthRealizer line 143
  39. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_correctionWidth line 146
  40. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.wordWidth line 149
  41. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.wordWidthRealizer line 150
  42. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.polynomial_wordWidth line 156
  43. def OAI.ContingencyTables.RootedEstimatorLayoutProgram.data line 168
  44. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.frames_data line 172
  45. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.binWidth_data line 181
  46. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.assignmentCount_data line 188
  47. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.ratioWidth_data line 195
  48. lemma OAI.ContingencyTables.RootedEstimatorLayoutProgram.correctionWalkWidth_data line 201