OAI/Combinatorics/KMedianRecovery/Recovery/ThresholdTimesPower.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.Anchoring.threshold_times_power line 9
  2. lemma OAI.MetricKMedianRecovery.Anchoring.threshold_count_factor line 14
  3. lemma OAI.MetricKMedianRecovery.Anchoring.selected_count_bound line 29
  4. theorem OAI.MetricKMedianRecovery.Anchoring.threshold_with_count line 48
  5. def OAI.MetricKMedianRecovery.Anchoring.separation line 67
  6. def OAI.MetricKMedianRecovery.Anchoring.cluster line 68
  7. def OAI.MetricKMedianRecovery.Anchoring.clusterWeight line 70
  8. def OAI.MetricKMedianRecovery.Anchoring.ballFacilities line 72
  9. lemma OAI.MetricKMedianRecovery.Anchoring.separation_le line 75
  10. lemma OAI.MetricKMedianRecovery.Anchoring.separation_pos line 78
  11. lemma OAI.MetricKMedianRecovery.Anchoring.clusterWeight_nonneg line 87
  12. lemma OAI.MetricKMedianRecovery.Anchoring.nearest_cluster_radius line 91
  13. lemma OAI.MetricKMedianRecovery.Anchoring.good_radius_bound line 102
  14. lemma OAI.MetricKMedianRecovery.Anchoring.ballFacilities_disjoint line 118
  15. lemma OAI.MetricKMedianRecovery.Anchoring.proxy_in_ball line 131
  16. lemma OAI.MetricKMedianRecovery.Anchoring.proxies_injective line 139
  17. lemma OAI.MetricKMedianRecovery.Anchoring.crowded_card_bound line 149