OAI/Combinatorics/KMedianRecovery/Recovery/StepPack.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.bf_pack line 16
2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.sf_pack line 18
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.mapped_pack line 20
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.Q_pack line 23
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.power_pack line 27
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.base_pack line 31
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.tails_pack line 36
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.W_pack line 41
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.ctx_pack line 57
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.a_pack line 61
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.banks_pack line 65
12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.keys_pack line 70
13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.c_pack line 75
14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.crossInput_pack line 80
15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.finishInput_pack line 88
16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.advanceInput_pack line 97
17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.fallbackInput_pack line 103
18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.cross_pack line 118
19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledStep.run_pack line 154