OAI/Combinatorics/KMedianRecovery/Encoding/ExchangeIndex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedianRecovery.LocalSearch.ExchangeIndex line 9
2. def OAI.MetricKMedianRecovery.LocalSearch.classSlots line 11
3. def OAI.MetricKMedianRecovery.LocalSearch.auxiliarySlots line 13
4. def OAI.MetricKMedianRecovery.LocalSearch.exchangeWeight line 15
5. def OAI.MetricKMedianRecovery.LocalSearch.exchangeRemove line 19
6. def OAI.MetricKMedianRecovery.LocalSearch.exchangeAdd line 22
7. lemma OAI.MetricKMedianRecovery.LocalSearch.auxiliary_slot_mem line 27
8. lemma OAI.MetricKMedianRecovery.LocalSearch.auxiliary_card line 38
9. lemma OAI.MetricKMedianRecovery.LocalSearch.imageClass_pos line 45
10. lemma OAI.MetricKMedianRecovery.LocalSearch.exchangeWeight_nonneg line 50
11. lemma OAI.MetricKMedianRecovery.LocalSearch.exchange_width line 63
12. lemma OAI.MetricKMedianRecovery.LocalSearch.exchange_preserves_image line 76
13. lemma OAI.MetricKMedianRecovery.LocalSearch.total_addition_weight line 100