OAI/Combinatorics/KMedian/Optimization/ApproximateFractional.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.TruncatedLP.penalty line 13
  2. def OAI.MetricKMedian.TruncatedLP.loss line 15
  3. theorem OAI.MetricKMedian.TruncatedLP.penalty_pos line 17
  4. theorem OAI.MetricKMedian.TruncatedLP.penalty_one line 21
  5. theorem OAI.MetricKMedian.TruncatedLP.loss_bounds line 24
  6. theorem OAI.MetricKMedian.TruncatedLP.repair_error line 51
  7. structure OAI.MetricKMedian.TruncatedLP.FractionalData line 74
  8. def OAI.MetricKMedian.TruncatedLP.approximation line 78
  9. theorem OAI.MetricKMedian.TruncatedLP.approximation_spec line 89