OAI/Combinatorics/KMedianRecovery/Geometry/IndexedCost.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.PhaseSurplusProducer.indexed_cost line 13
2. lemma OAI.MetricKMedianRecovery.PhaseSurplusProducer.dual_on_points line 18
3. lemma OAI.MetricKMedianRecovery.PhaseSurplusProducer.strict_on_points line 25
4. lemma OAI.MetricKMedianRecovery.PhaseSurplusProducer.cluster_ge_one line 47
5. lemma OAI.MetricKMedianRecovery.PhaseSurplusProducer.comparison_ge_one line 56
6. lemma OAI.MetricKMedianRecovery.PhaseSurplusProducer.countConstant_ge_ten line 63
7. lemma OAI.MetricKMedianRecovery.PhaseSurplusProducer.pad_and_descend line 68
8. lemma OAI.MetricKMedianRecovery.PhaseSurplusProducer.normal_cost line 84
9. lemma OAI.MetricKMedianRecovery.PhaseSurplusProducer.small_cost line 127