OAI/Combinatorics/KMedian/Reduction/DeletionGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Reduction.Serving line 15
  2. theorem OAI.MetricKMedian.Reduction.serving_exists line 22
  3. def OAI.MetricKMedian.Reduction.Serving.radius line 53
  4. theorem OAI.MetricKMedian.Reduction.Serving.radius_nonneg line 55
  5. theorem OAI.MetricKMedian.Reduction.Serving.radius_pos line 57
  6. def OAI.MetricKMedian.Reduction.Serving.group line 65
  7. def OAI.MetricKMedian.Reduction.Serving.groupCost line 68
  8. theorem OAI.MetricKMedian.Reduction.Serving.groupCost_nonneg line 71
  9. theorem OAI.MetricKMedian.Reduction.Serving.groupCost_total line 74
  10. theorem OAI.MetricKMedian.Reduction.Serving.deletion_bound line 80