OAI/Combinatorics/ContingencyTables/Rooted/RootedCorrectionProgram.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

The executed selected-root correction

The stored grid point and sampled integer point share their literal capacity, forest, baseline and small-view arrays. The program computes the grid exponent, point penalty and population factor before the bounded rational power approximation.

  1. abbrev OAI.ContingencyTables.RootedCorrectionProgram.State line 22
  2. abbrev OAI.ContingencyTables.RootedCorrectionProgram.Input line 23
  3. def OAI.ContingencyTables.RootedCorrectionProgram.exponentInput line 25
  4. def OAI.ContingencyTables.RootedCorrectionProgram.exponentInputRealizer line 27
  5. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_exponentInput line 31
  6. def OAI.ContingencyTables.RootedCorrectionProgram.pointInput line 43
  7. def OAI.ContingencyTables.RootedCorrectionProgram.pointInputRealizer line 46
  8. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_pointInput line 56
  9. def OAI.ContingencyTables.RootedCorrectionProgram.binInput line 67
  10. def OAI.ContingencyTables.RootedCorrectionProgram.binInputRealizer line 69
  11. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_binInput line 76
  12. def OAI.ContingencyTables.RootedCorrectionProgram.populationInput line 92
  13. def OAI.ContingencyTables.RootedCorrectionProgram.populationInputRealizer line 94
  14. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_populationInput line 98
  15. def OAI.ContingencyTables.RootedCorrectionProgram.phase line 103
  16. def OAI.ContingencyTables.RootedCorrectionProgram.phaseRealizer line 105
  17. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_phase line 110
  18. def OAI.ContingencyTables.RootedCorrectionProgram.exponentValue line 120
  19. def OAI.ContingencyTables.RootedCorrectionProgram.exponentValueRealizer line 122
  20. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_exponentValue line 125
  21. def OAI.ContingencyTables.RootedCorrectionProgram.pointValue line 128
  22. def OAI.ContingencyTables.RootedCorrectionProgram.pointValueRealizer line 130
  23. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_pointValue line 133
  24. def OAI.ContingencyTables.RootedCorrectionProgram.populationValue line 136
  25. def OAI.ContingencyTables.RootedCorrectionProgram.populationValueRealizer line 138
  26. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_populationValue line 141
  27. def OAI.ContingencyTables.RootedCorrectionProgram.frame line 146
  28. def OAI.ContingencyTables.RootedCorrectionProgram.frameRealizer line 148
  29. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_frame line 150
  30. def OAI.ContingencyTables.RootedCorrectionProgram.prepare line 155
  31. def OAI.ContingencyTables.RootedCorrectionProgram.prepareRealizer line 156
  32. lemma OAI.ContingencyTables.RootedCorrectionProgram.polynomial_prepare line 157
  33. def OAI.ContingencyTables.RootedCorrectionProgram.output line 160
  34. def OAI.ContingencyTables.RootedCorrectionProgram.outputRealizer line 161
  35. theorem OAI.ContingencyTables.RootedCorrectionProgram.polynomial_output line 164