OAI/Combinatorics/KMedianRecovery/Recovery/ClassSlotsMem.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.LocalSearch.classSlots_mem line 10
2. lemma OAI.MetricKMedianRecovery.LocalSearch.removal_weight_at_slot line 19
3. lemma OAI.MetricKMedianRecovery.LocalSearch.removal_weight_le line 51
4. def OAI.MetricKMedianRecovery.LocalSearch.connection line 98
5. def OAI.MetricKMedianRecovery.LocalSearch.cost line 100
6. lemma OAI.MetricKMedianRecovery.LocalSearch.connection_nonneg line 102
7. lemma OAI.MetricKMedianRecovery.LocalSearch.connection_le line 107
8. lemma OAI.MetricKMedianRecovery.LocalSearch.cost_nonneg line 110
9. lemma OAI.MetricKMedianRecovery.LocalSearch.connection_mono line 112
10. lemma OAI.MetricKMedianRecovery.LocalSearch.cost_mono line 116
11. def OAI.MetricKMedianRecovery.LocalSearch.nearest line 119
12. lemma OAI.MetricKMedianRecovery.LocalSearch.nearest_mem line 121
13. lemma OAI.MetricKMedianRecovery.LocalSearch.nearest_distance line 123
14. def OAI.MetricKMedianRecovery.LocalSearch.WidthLocalMin line 132
15. lemma OAI.MetricKMedianRecovery.LocalSearch.padded_not_worse line 135
16. lemma OAI.MetricKMedianRecovery.LocalSearch.local_min_le_smaller line 152
17. lemma OAI.MetricKMedianRecovery.LocalSearch.exchange_card_le line 161
18. lemma OAI.MetricKMedianRecovery.LocalSearch.exchange_diff_bounds line 166
19. lemma OAI.MetricKMedianRecovery.LocalSearch.local_exchange line 178