OAI/Combinatorics/KMedianRecovery/Encoding/HistoryBits.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.historyBits line 11
2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.historyBits_append line 13
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.chunk line 16
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.chunk_computes line 18
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.chunk_pack line 24
6. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.step line 31
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.step_computes line 33
8. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.pack line 36
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.step_pack line 39
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.iterate_pack line 46
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.history_length line 55
12. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.capPoly line 74
13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.iterate_length line 76
14. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.cap line 98
15. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.run line 99
16. def OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.run_computes line 101
17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryHistoryRun.run_pack line 104