OAI/Combinatorics/KMedianRecovery/Recovery/InitialPack.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.high_pack line 20
2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.far_pack line 23
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.ctx_pack line 26
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loInput_pack line 28
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loCount_pack line 32
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loHistory_pack line 35
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loFinish_pack line 38
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.bracketInput_pack line 43
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.bracket_pack line 47
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.prices_pack line 50
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.inputs_pack line 52
12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.counts_pack line 56
13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.histories_pack line 60
14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.finishes_pack line 64
15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.initialState_pack line 70
16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.loopInput_pack line 76