OAI/Combinatorics/KMedianRecovery/Recovery/Op.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.length_encode_reverse line 11
2. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.length_encode_zip line 13
3. def OAI.MetricKMedianRecovery.BitMachine.WordList.Zip.op line 26
4. def OAI.MetricKMedianRecovery.BitMachine.WordList.Zip.op_computes line 31
5. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Zip.op_nil line 40
6. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Zip.op_cons line 43
7. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Zip.fold_eq line 48
8. def OAI.MetricKMedianRecovery.BitMachine.WordList.Zip.run line 65
9. def OAI.MetricKMedianRecovery.BitMachine.WordList.Zip.run_computes line 67
10. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Zip.run_encode line 72
11. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.dotListsWords line 94
12. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.dotListsWords_computes line 95
13. lemma OAI.MetricKMedianRecovery.BitMachine.IntegerArray.dotListsWords_encode line 96
14. def OAI.MetricKMedianRecovery.BitMachine.IntegerArray.dotLists line 100
15. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.encode_le_bound line 108
16. def OAI.MetricKMedianRecovery.BitMachine.WordList.Indices.op line 119
17. def OAI.MetricKMedianRecovery.BitMachine.WordList.Indices.op_computes line 122
18. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Indices.op_pair line 130
19. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Indices.fold_eq line 134
20. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Indices.bits_length_le line 144
21. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Indices.range_length line 147
22. def OAI.MetricKMedianRecovery.BitMachine.WordList.Indices.run line 155
23. def OAI.MetricKMedianRecovery.BitMachine.WordList.Indices.run_computes line 157
24. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.Indices.run_encode line 162