OAI/Combinatorics/KMedianRecovery/Recovery/ZeroClasses.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.LocalSearch.zeroClasses line 10
2. lemma OAI.MetricKMedianRecovery.LocalSearch.zero_class_eq line 14
3. lemma OAI.MetricKMedianRecovery.LocalSearch.zero_cost_connection line 17
4. lemma OAI.MetricKMedianRecovery.LocalSearch.zero_cost_classes line 21
5. theorem OAI.MetricKMedianRecovery.LocalSearch.zero_classes_solution line 31
6. theorem OAI.MetricKMedianRecovery.LocalSearch.optimum_zero_iff line 60
7. lemma OAI.MetricKMedianRecovery.RoundedAssembly.successful_factor_nonneg line 82
8. lemma OAI.MetricKMedianRecovery.RoundedAssembly.successful_factor_le_five line 86
9. lemma OAI.MetricKMedianRecovery.RoundedAssembly.rounded_successful_factor line 90
10. lemma OAI.MetricKMedianRecovery.RoundedAssembly.rounded_fallback_factor line 95
11. theorem OAI.MetricKMedianRecovery.RoundedAssembly.rounded_calls line 98