OAI/Combinatorics/KMedianRecovery/Branching/BranchChecksCorrect.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.WordList.encode_eq_nil_iff line 7
2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFinSet.encode_eq_nil_iff line 13
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.outside_nil line 27
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badBalls_nil line 29
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.badRadii_nil line 33
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchCheck.run_pack line 36
7. lemma OAI.MetricKMedianRecovery.BlueDP.best_some_of_plan line 49
8. lemma OAI.MetricKMedianRecovery.BlueDP.plan_value_unique line 59
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionAlgorithm.choices_binary line 70
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionAlgorithm.sixtyTwoFin line 87
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletionAlgorithm.choices_expected line 108