OAI/Combinatorics/ContingencyTables/Rooted/RootedRatioSampleProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial execution of an adjacent-parameter ratio sample

The exact ratio is either one or one half. The program compares the two computed integer exponents and never materializes an exponential weight.

  1. abbrev OAI.ContingencyTables.RootedRatioSampleProgram.Input line 17
  2. def OAI.ContingencyTables.RootedRatioSampleProgram.bump line 19
  3. def OAI.ContingencyTables.RootedRatioSampleProgram.bumpRealizer line 20
  4. lemma OAI.ContingencyTables.RootedRatioSampleProgram.polynomial_bump line 24
  5. def OAI.ContingencyTables.RootedRatioSampleProgram.equalExponents line 35
  6. def OAI.ContingencyTables.RootedRatioSampleProgram.equalExponentsRealizer line 37
  7. lemma OAI.ContingencyTables.RootedRatioSampleProgram.polynomial_equalExponents line 43
  8. def OAI.ContingencyTables.RootedRatioSampleProgram.ratio line 48
  9. def OAI.ContingencyTables.RootedRatioSampleProgram.ratioRealizer line 49
  10. lemma OAI.ContingencyTables.RootedRatioSampleProgram.polynomial_ratio line 51
  11. abbrev OAI.ContingencyTables.RootedRatioSampleProgram.SampleInput line 54
  12. def OAI.ContingencyTables.RootedRatioSampleProgram.currentInput line 56
  13. def OAI.ContingencyTables.RootedRatioSampleProgram.currentInputRealizer line 58
  14. lemma OAI.ContingencyTables.RootedRatioSampleProgram.polynomial_currentInput line 63
  15. def OAI.ContingencyTables.RootedRatioSampleProgram.output line 67
  16. def OAI.ContingencyTables.RootedRatioSampleProgram.outputRealizer line 68
  17. theorem OAI.ContingencyTables.RootedRatioSampleProgram.polynomial_output line 70
  18. lemma OAI.ContingencyTables.RootedRatioSampleProgram.exponent_step line 80
  19. lemma OAI.ContingencyTables.RootedRatioSampleProgram.ratio_data line 123
  20. theorem OAI.ContingencyTables.RootedRatioSampleProgram.output_data line 148