OAI/Combinatorics/KMedianRecovery/Recovery/SingleRadiusRatio.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.single_radius_ratio line 11
2. def OAI.MetricKMedianRecovery.Sampling.Comparison.leaderPair line 38
3. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.leaderPair_spec line 41
4. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_population_sum line 46
5. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_completion_sum line 96
6. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.uncovered_completion_sum line 143