OAI/Combinatorics/KMedianRecovery/Recovery/Answer.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.answer line 8
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.answer_computes line 10
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.answer_pack line 12
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.step line 17
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.step_computes line 19
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.step_pack line 24
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.finish_none line 33
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.iterate_pack line 38
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.member_length_le line 49
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.indices_length line 57
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.finset_indices_length line 64
12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.context_length_change line 69
13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.dimensions line 77
14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFinish.initial_budget_length line 91