OAI/Combinatorics/KMedianRecovery/Recovery/DyadicGrid.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.DyadicGrid.State line 7
  2. def OAI.MetricKMedianRecovery.DyadicGrid.point line 8
  3. def OAI.MetricKMedianRecovery.DyadicGrid.interval line 9
  4. def OAI.MetricKMedianRecovery.DyadicGrid.advance line 10
  5. def OAI.MetricKMedianRecovery.DyadicGrid.start line 13
  6. lemma OAI.MetricKMedianRecovery.DyadicGrid.point_double line 14
  7. lemma OAI.MetricKMedianRecovery.DyadicGrid.point_mid line 19
  8. lemma OAI.MetricKMedianRecovery.DyadicGrid.advance_interval line 26
  9. lemma OAI.MetricKMedianRecovery.DyadicGrid.advance_bounds line 31
  10. lemma OAI.MetricKMedianRecovery.DyadicGrid.iterate_bounds line 36
  11. lemma OAI.MetricKMedianRecovery.DyadicGrid.search_iterate line 46
  12. lemma OAI.MetricKMedianRecovery.DyadicGrid.iterate_interval line 51