OAI/Combinatorics/KMedianRecovery/Recovery/DecisionOps.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.not line 9
2. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.and line 15
3. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.or line 22
4. def OAI.MetricKMedianRecovery.BitMachine.NatOps.lt line 30
5. def OAI.MetricKMedianRecovery.BitMachine.RatOps.lt line 35
6. def OAI.MetricKMedianRecovery.BitMachine.RatOps.eq line 40
7. lemma OAI.MetricKMedianRecovery.PriceBisection.search_eq_iterate line 53
8. lemma OAI.MetricKMedianRecovery.PriceBisection.iterate_dyadic line 59
9. lemma OAI.MetricKMedianRecovery.PriceBisection.dyadic_height line 88
10. lemma OAI.MetricKMedianRecovery.PriceBisection.iterate_height line 99
11. lemma OAI.MetricKMedianRecovery.PriceBisection.clog_two_bits line 109