OAI/Combinatorics/KMedianRecovery/Recovery/Threshold.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.Anchoring.geometric_half_sum line 7
  2. lemma OAI.MetricKMedianRecovery.Anchoring.geometric_half_tail line 23
  3. def OAI.MetricKMedianRecovery.Anchoring.threshold line 45
  4. def OAI.MetricKMedianRecovery.Anchoring.rounds line 46
  5. def OAI.MetricKMedianRecovery.Anchoring.countConstant line 47
  6. def OAI.MetricKMedianRecovery.Anchoring.shortCenters line 52
  7. def OAI.MetricKMedianRecovery.Anchoring.badCenters line 54
  8. lemma OAI.MetricKMedianRecovery.Anchoring.bad_count_pointwise line 57
  9. lemma OAI.MetricKMedianRecovery.Anchoring.threshold_total_bound line 76
  10. lemma OAI.MetricKMedianRecovery.Anchoring.threshold_pos line 118
  11. lemma OAI.MetricKMedianRecovery.Anchoring.threshold_le line 120
  12. lemma OAI.MetricKMedianRecovery.Anchoring.rounds_bound line 123
  13. lemma OAI.MetricKMedianRecovery.Anchoring.rounds_pos line 126
  14. theorem OAI.MetricKMedianRecovery.Anchoring.selected_threshold line 133