OAI/Combinatorics/KMedian/Optimization/ApproximateLPSelection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.TruncatedLP.FractionalData.Valid line 14
  2. instance OAI.MetricKMedian.TruncatedLP.(instance at line 21) line 21
  3. def OAI.MetricKMedian.TruncatedLP.FractionalData.value line 24
  4. def OAI.MetricKMedian.TruncatedLP.scaledCandidate line 27
  5. def OAI.MetricKMedian.TruncatedLP.feasibleScales line 33
  6. def OAI.MetricKMedian.TruncatedLP.selectFractional line 38
  7. theorem OAI.MetricKMedian.TruncatedLP.value_div line 45
  8. theorem OAI.MetricKMedian.TruncatedLP.candidate_success line 49
  9. theorem OAI.MetricKMedian.TruncatedLP.selectFractional_spec line 70
  10. theorem OAI.MetricKMedian.TruncatedLP.feasibleScales_card line 82