OAI/Combinatorics/KMedianRecovery/Recovery/BadClientWeighted.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.LocalSearch.bad_client_weighted line 8
2. lemma OAI.MetricKMedianRecovery.LocalSearch.good_client_weighted line 33
3. lemma OAI.MetricKMedianRecovery.LocalSearch.bad_routing_change line 58
4. lemma OAI.MetricKMedianRecovery.LocalSearch.good_routing_change line 86
5. theorem OAI.MetricKMedianRecovery.LocalSearch.weighted_swap_family line 100
6. lemma OAI.MetricKMedianRecovery.LocalSearch.weighted_swap_sum_form line 143