OAI/Combinatorics/ContingencyTables/Rooted/RootedEstimatorWordProgram.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

One flat word executes the complete weight estimator

The number of generated rows is bounded by the supplied word length. The binary schedule therefore remains safe even on malformed inputs.

  1. abbrev OAI.ContingencyTables.RootedEstimatorWordProgram.Input line 16
  2. def OAI.ContingencyTables.RootedEstimatorWordProgram.phase line 18
  3. def OAI.ContingencyTables.RootedEstimatorWordProgram.phaseRealizer line 20
  4. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_phase line 29
  5. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioPrefix line 48
  6. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioPrefixRealizer line 49
  7. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_ratioPrefix line 54
  8. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioRows line 58
  9. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioRowsRealizer line 59
  10. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_ratioRows line 63
  11. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioChunk line 68
  12. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioChunkRealizer line 70
  13. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_ratioChunk line 78
  14. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioState line 85
  15. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioStateRealizer line 86
  16. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_ratioState line 89
  17. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioWords line 94
  18. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioWordsRealizer line 95
  19. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_ratioWords line 99
  20. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioBlock line 104
  21. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioBlockRealizer line 106
  22. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_ratioBlock line 110
  23. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioBlocks line 114
  24. def OAI.ContingencyTables.RootedEstimatorWordProgram.ratioBlocksRealizer line 116
  25. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_ratioBlocks line 118
  26. def OAI.ContingencyTables.RootedEstimatorWordProgram.correctionTail line 122
  27. def OAI.ContingencyTables.RootedEstimatorWordProgram.correctionTailRealizer line 123
  28. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_correctionTail line 128
  29. def OAI.ContingencyTables.RootedEstimatorWordProgram.correctionWords line 132
  30. def OAI.ContingencyTables.RootedEstimatorWordProgram.correctionWordsRealizer line 134
  31. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_correctionWords line 143
  32. def OAI.ContingencyTables.RootedEstimatorWordProgram.terminalState line 153
  33. def OAI.ContingencyTables.RootedEstimatorWordProgram.terminalStateRealizer line 154
  34. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_terminalState line 158
  35. def OAI.ContingencyTables.RootedEstimatorWordProgram.correctionSample line 164
  36. def OAI.ContingencyTables.RootedEstimatorWordProgram.correctionSampleRealizer line 167
  37. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_correctionSample line 178
  38. def OAI.ContingencyTables.RootedEstimatorWordProgram.correctionBlock line 195
  39. def OAI.ContingencyTables.RootedEstimatorWordProgram.correctionBlockRealizer line 197
  40. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_correctionBlock line 199
  41. def OAI.ContingencyTables.RootedEstimatorWordProgram.prepare line 203
  42. def OAI.ContingencyTables.RootedEstimatorWordProgram.prepareRealizer line 205
  43. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_prepare line 208
  44. def OAI.ContingencyTables.RootedEstimatorWordProgram.output line 215
  45. def OAI.ContingencyTables.RootedEstimatorWordProgram.outputRealizer line 216
  46. theorem OAI.ContingencyTables.RootedEstimatorWordProgram.polynomial_output line 219
  47. lemma OAI.ContingencyTables.RootedEstimatorWordProgram.phase_data line 227