OAI/Combinatorics/ContingencyTables/Machines/BoundedBinarySearch.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Binary search for the attained endpoint of a monotone feasibility test

A fixed number of midpoint tests finds a known cutoff. The number of tests is logarithmic in the binary upper bound; no values are enumerated.

  1. abbrev OAI.ContingencyTables.BoundedBinarySearch.Window line 17
  2. def OAI.ContingencyTables.BoundedBinarySearch.midpoint line 19
  3. def OAI.ContingencyTables.BoundedBinarySearch.step line 21
  4. def OAI.ContingencyTables.BoundedBinarySearch.run line 24
  5. lemma OAI.ContingencyTables.BoundedBinarySearch.step_width line 28
  6. lemma OAI.ContingencyTables.BoundedBinarySearch.run_width line 34
  7. lemma OAI.ContingencyTables.BoundedBinarySearch.step_contains line 49
  8. lemma OAI.ContingencyTables.BoundedBinarySearch.run_contains line 61
  9. theorem OAI.ContingencyTables.BoundedBinarySearch.run_eq_cutoff line 71
  10. def OAI.ContingencyTables.BoundedBinarySearch.find line 84
  11. theorem OAI.ContingencyTables.BoundedBinarySearch.find_eq_cutoff line 87