OAI/Combinatorics/ContingencyTables/Machines/DyadicRootProgram.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Polynomial binary execution of the rational correction bisection

The root degree is the length of a supplied allowance list. One fixed depth list controls the outer loop. Thus both natural-power evaluation and the bisection loop have polynomial cost in the supplied binary data and the two explicit allowances.

  1. def OAI.ContingencyTables.DyadicRootProgram.powerInput line 20
  2. def OAI.ContingencyTables.DyadicRootProgram.powerInputRealizer line 21
  3. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_powerInput line 22
  4. def OAI.ContingencyTables.DyadicRootProgram.markedPower line 27
  5. def OAI.ContingencyTables.DyadicRootProgram.markedPowerRealizer line 28
  6. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_markedPower line 31
  7. lemma OAI.ContingencyTables.DyadicRootProgram.markedPower_eq line 40
  8. abbrev OAI.ContingencyTables.DyadicRootProgram.Parameters line 43
  9. abbrev OAI.ContingencyTables.DyadicRootProgram.State line 44
  10. def OAI.ContingencyTables.DyadicRootProgram.lowRealizer line 46
  11. def OAI.ContingencyTables.DyadicRootProgram.highRealizer line 48
  12. def OAI.ContingencyTables.DyadicRootProgram.denominatorRealizer line 50
  13. def OAI.ContingencyTables.DyadicRootProgram.numeratorRealizer line 51
  14. def OAI.ContingencyTables.DyadicRootProgram.targetDenominatorRealizer line 53
  15. def OAI.ContingencyTables.DyadicRootProgram.allowanceRealizer line 55
  16. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_low line 57
  17. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_high line 58
  18. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_denominator line 59
  19. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_numerator line 61
  20. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_targetDenominator line 63
  21. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_allowance line 65
  22. def OAI.ContingencyTables.DyadicRootProgram.mid line 68
  23. def OAI.ContingencyTables.DyadicRootProgram.midRealizer line 69
  24. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_mid line 70
  25. def OAI.ContingencyTables.DyadicRootProgram.twiceDenominator line 73
  26. def OAI.ContingencyTables.DyadicRootProgram.twiceDenominatorRealizer line 74
  27. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_twiceDenominator line 77
  28. def OAI.ContingencyTables.DyadicRootProgram.leftProduct line 81
  29. def OAI.ContingencyTables.DyadicRootProgram.leftProductRealizer line 82
  30. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_leftProduct line 86
  31. def OAI.ContingencyTables.DyadicRootProgram.rightProduct line 91
  32. def OAI.ContingencyTables.DyadicRootProgram.rightProductRealizer line 92
  33. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_rightProduct line 95
  34. def OAI.ContingencyTables.DyadicRootProgram.test line 100
  35. def OAI.ContingencyTables.DyadicRootProgram.testRealizer line 101
  36. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_test line 102
  37. def OAI.ContingencyTables.DyadicRootProgram.lowerBranchRealizer line 106
  38. def OAI.ContingencyTables.DyadicRootProgram.upperBranchRealizer line 112
  39. def OAI.ContingencyTables.DyadicRootProgram.next line 119
  40. def OAI.ContingencyTables.DyadicRootProgram.nextRealizer line 122
  41. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_next line 125
  42. lemma OAI.ContingencyTables.DyadicRootProgram.next_eq line 135
  43. def OAI.ContingencyTables.DyadicRootProgram.height line 140
  44. lemma OAI.ContingencyTables.DyadicRootProgram.size_double line 142
  45. lemma OAI.ContingencyTables.DyadicRootProgram.height_advance line 145
  46. def OAI.ContingencyTables.DyadicRootProgram.advance line 154
  47. def OAI.ContingencyTables.DyadicRootProgram.advanceRealizer line 155
  48. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_advance line 156
  49. lemma OAI.ContingencyTables.DyadicRootProgram.fold_parameters line 159
  50. lemma OAI.ContingencyTables.DyadicRootProgram.fold_height line 165
  51. lemma OAI.ContingencyTables.DyadicRootProgram.height_le_weight line 179
  52. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_loop line 187
  53. abbrev OAI.ContingencyTables.DyadicRootProgram.Input line 217
  54. def OAI.ContingencyTables.DyadicRootProgram.prepare line 218
  55. def OAI.ContingencyTables.DyadicRootProgram.prepareRealizer line 219
  56. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_prepare line 220
  57. def OAI.ContingencyTables.DyadicRootProgram.execute line 225
  58. def OAI.ContingencyTables.DyadicRootProgram.executeRealizer line 226
  59. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_execute line 227
  60. def OAI.ContingencyTables.DyadicRootProgram.finish line 230
  61. def OAI.ContingencyTables.DyadicRootProgram.finishRealizer line 232
  62. lemma OAI.ContingencyTables.DyadicRootProgram.polynomial_finish line 234
  63. def OAI.ContingencyTables.DyadicRootProgram.output line 238
  64. def OAI.ContingencyTables.DyadicRootProgram.outputRealizer line 239
  65. theorem OAI.ContingencyTables.DyadicRootProgram.polynomial_output line 240
  66. lemma OAI.ContingencyTables.DyadicRootProgram.fold_eq line 243
  67. theorem OAI.ContingencyTables.DyadicRootProgram.output_eq line 254
  68. theorem OAI.ContingencyTables.DyadicRootProgram.output_value line 264