OAI/Combinatorics/KMedianRecovery/Algorithms/BudgetBound.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.budget_bound line 13
2. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.active_insert line 25
3. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.inactive_distance line 40
4. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.admissible_insert line 58
5. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.payment_insert line 77
6. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.dual_insert line 91
7. theorem OAI.MetricKMedianRecovery.UniformRowDisabling.openable_insert line 99
8. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.entry_insert line 109
9. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.prefix_insert line 130
10. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.valid_insert line 146
11. theorem OAI.MetricKMedianRecovery.UniformRowDisabling.history_insert line 165
12. lemma OAI.MetricKMedianRecovery.UniformRowDisabling.attains_insert line 182