OAI/Combinatorics/KMedianRecovery/Recovery/DisjointPool.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.PhaseCountCrossing.disjoint_pool line 11
2. theorem OAI.MetricKMedianRecovery.PhaseCountCrossing.regular_phase_crossing line 20
3. def OAI.MetricKMedianRecovery.PriceBisection.refine line 47
4. def OAI.MetricKMedianRecovery.PriceBisection.search line 51
5. lemma OAI.MetricKMedianRecovery.PriceBisection.refine_bounds line 55
6. lemma OAI.MetricKMedianRecovery.PriceBisection.refine_width line 64
7. lemma OAI.MetricKMedianRecovery.PriceBisection.refine_bracket line 69
8. lemma OAI.MetricKMedianRecovery.PriceBisection.search_spec line 77
9. def OAI.MetricKMedianRecovery.PriceBisection.iterations line 96
10. lemma OAI.MetricKMedianRecovery.PriceBisection.iterations_precision line 98
11. theorem OAI.MetricKMedianRecovery.PriceBisection.close_bracket line 107