OAI/Combinatorics/KMedianRecovery/Branching/BluePlan.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BlueDP.spec_mono line 10
2. lemma OAI.MetricKMedianRecovery.BlueDP.recurrence_spec line 15
3. lemma OAI.MetricKMedianRecovery.BlueDP.best_spec line 39
4. def OAI.MetricKMedianRecovery.BlueDP.pick line 49
5. lemma OAI.MetricKMedianRecovery.BlueDP.pick_mem line 52
6. lemma OAI.MetricKMedianRecovery.BlueDP.pick_eq line 62
7. lemma OAI.MetricKMedianRecovery.BlueDP.cost_pick line 67
8. def OAI.MetricKMedianRecovery.BlueDP.makePlan line 76
9. lemma OAI.MetricKMedianRecovery.BlueDP.route_length line 106
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueSize.atom_bound line 114
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueSize.candidate_bound line 131