OAI/Combinatorics/ContingencyTables/Machines/BinarySearchProgram.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

A polynomial binary program for monotone endpoint search

The supplied test is a realized binary predicate. The loop performs one midpoint test per bit of the upper bound and keeps the unchanged test data throughout.

  1. def OAI.ContingencyTables.BinarySearchProgram.midpointRealizer line 17
  2. lemma OAI.ContingencyTables.BinarySearchProgram.polynomial_midpoint line 21
  3. abbrev OAI.ContingencyTables.BinarySearchProgram.State line 32
  4. def OAI.ContingencyTables.BinarySearchProgram.advance line 34
  5. def OAI.ContingencyTables.BinarySearchProgram.advanceRealizer line 37
  6. lemma OAI.ContingencyTables.BinarySearchProgram.polynomial_advance line 49
  7. lemma OAI.ContingencyTables.BinarySearchProgram.midpoint_le_max line 70
  8. lemma OAI.ContingencyTables.BinarySearchProgram.step_le_max line 75
  9. lemma OAI.ContingencyTables.BinarySearchProgram.fold_context line 82
  10. lemma OAI.ContingencyTables.BinarySearchProgram.fold_bounds line 89
  11. lemma OAI.ContingencyTables.BinarySearchProgram.polynomial_loop line 100
  12. def OAI.ContingencyTables.BinarySearchProgram.steps line 130
  13. def OAI.ContingencyTables.BinarySearchProgram.stepsRealizer line 132
  14. lemma OAI.ContingencyTables.BinarySearchProgram.polynomial_steps line 135
  15. def OAI.ContingencyTables.BinarySearchProgram.prepare line 141
  16. def OAI.ContingencyTables.BinarySearchProgram.prepareRealizer line 143
  17. lemma OAI.ContingencyTables.BinarySearchProgram.polynomial_prepare line 146
  18. def OAI.ContingencyTables.BinarySearchProgram.execute line 150
  19. def OAI.ContingencyTables.BinarySearchProgram.executeRealizer line 153
  20. lemma OAI.ContingencyTables.BinarySearchProgram.polynomial_execute line 158
  21. def OAI.ContingencyTables.BinarySearchProgram.search line 161
  22. def OAI.ContingencyTables.BinarySearchProgram.searchRealizer line 163
  23. lemma OAI.ContingencyTables.BinarySearchProgram.polynomial_search line 167
  24. lemma OAI.ContingencyTables.BinarySearchProgram.fold_code line 172
  25. theorem OAI.ContingencyTables.BinarySearchProgram.search_eq line 183