OAI/Combinatorics/ContingencyTables/Rooted/RootedCorrectionSampleProgram.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Executing one selected-root correction sample

Separate finite words drive the grid walk and the integer draw. The computed final bin and sampled integer are then passed to the exact population and rational-power correction program.

  1. abbrev OAI.ContingencyTables.RootedCorrectionSampleProgram.State line 19
  2. abbrev OAI.ContingencyTables.RootedCorrectionSampleProgram.Input line 20
  3. def OAI.ContingencyTables.RootedCorrectionSampleProgram.walked line 22
  4. def OAI.ContingencyTables.RootedCorrectionSampleProgram.walkedRealizer line 24
  5. lemma OAI.ContingencyTables.RootedCorrectionSampleProgram.polynomial_walked line 29
  6. def OAI.ContingencyTables.RootedCorrectionSampleProgram.binFrame line 37
  7. def OAI.ContingencyTables.RootedCorrectionSampleProgram.binFrameRealizer line 40
  8. lemma OAI.ContingencyTables.RootedCorrectionSampleProgram.polynomial_binFrame line 50
  9. def OAI.ContingencyTables.RootedCorrectionSampleProgram.sampled line 68
  10. def OAI.ContingencyTables.RootedCorrectionSampleProgram.sampledRealizer line 69
  11. lemma OAI.ContingencyTables.RootedCorrectionSampleProgram.polynomial_sampled line 74
  12. def OAI.ContingencyTables.RootedCorrectionSampleProgram.prepare line 81
  13. def OAI.ContingencyTables.RootedCorrectionSampleProgram.prepareRealizer line 83
  14. lemma OAI.ContingencyTables.RootedCorrectionSampleProgram.polynomial_prepare line 85
  15. def OAI.ContingencyTables.RootedCorrectionSampleProgram.output line 91
  16. def OAI.ContingencyTables.RootedCorrectionSampleProgram.outputRealizer line 92
  17. theorem OAI.ContingencyTables.RootedCorrectionSampleProgram.polynomial_output line 95
  18. def OAI.ContingencyTables.RootedCorrectionSampleProgram.data line 105
  19. lemma OAI.ContingencyTables.RootedCorrectionSampleProgram.walked_data line 110
  20. lemma OAI.ContingencyTables.RootedCorrectionSampleProgram.binFrame_data line 120
  21. lemma OAI.ContingencyTables.RootedCorrectionSampleProgram.sampled_data line 131
  22. lemma OAI.ContingencyTables.RootedCorrectionSampleProgram.bin_flatDraw line 145
  23. theorem OAI.ContingencyTables.RootedCorrectionSampleProgram.output_data line 158