OAI/Combinatorics/KMedianRecovery/Recovery/RawSlices.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.RawDrop.step line 8
2. def OAI.MetricKMedianRecovery.BitMachine.RawDrop.step_computes line 11
3. lemma OAI.MetricKMedianRecovery.BitMachine.RawDrop.decrement_length line 17
4. lemma OAI.MetricKMedianRecovery.BitMachine.RawDrop.first_step line 21
5. lemma OAI.MetricKMedianRecovery.BitMachine.RawDrop.rest_step line 25
6. lemma OAI.MetricKMedianRecovery.BitMachine.RawDrop.length_step line 29
7. lemma OAI.MetricKMedianRecovery.BitMachine.RawDrop.iterate_bounds line 38
8. lemma OAI.MetricKMedianRecovery.BitMachine.RawDrop.step_zero line 51
9. lemma OAI.MetricKMedianRecovery.BitMachine.RawDrop.step_succ line 53
10. def OAI.MetricKMedianRecovery.BitMachine.RawDrop.run line 57
11. def OAI.MetricKMedianRecovery.BitMachine.RawDrop.run_computes line 58
12. lemma OAI.MetricKMedianRecovery.BitMachine.RawDrop.drop_iterate line 73
13. lemma OAI.MetricKMedianRecovery.BitMachine.RawDrop.run_encode line 90
14. def OAI.MetricKMedianRecovery.BitMachine.RawTake.number line 99
15. def OAI.MetricKMedianRecovery.BitMachine.RawTake.number_computes line 101
16. def OAI.MetricKMedianRecovery.BitMachine.RawTake.run line 103
17. def OAI.MetricKMedianRecovery.BitMachine.RawTake.run_computes line 106
18. lemma OAI.MetricKMedianRecovery.BitMachine.RawTake.run_pack line 108
19. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.dropWords line 116
20. def OAI.MetricKMedianRecovery.BitMachine.UnaryTake.dropWords_computes line 117