OAI/Combinatorics/KMedianRecovery/Recovery/OrientedSearch.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reversedInput line 11
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reversedInput_computes line 13
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reversed line 16
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reversed_computes line 17
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reversed_pack line 19
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reverseContext line 23
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reverseContext_computes line 24
8. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reverseInput line 25
9. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reverseInput_computes line 27
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reverseInput_pack line 33
11. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reflect line 38
12. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reflect_computes line 41
13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reflect_pack line 44
14. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reverseRun line 48
15. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reverseRun_computes line 50
16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.reverseRun_pack line 52
17. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.isReversed line 61
18. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.isReversed_computes line 63
19. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.run line 66
20. def OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.run_computes line 68
21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOrientedSearch.run_pack line 70