OAI/Combinatorics/KMedian/Optimization/ApproximationListProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.LPBinary.Repair.Output line 13
  2. abbrev OAI.MetricKMedian.LPBinary.Repair.eo line 14
  3. def OAI.MetricKMedian.LPBinary.Repair.opening line 16
  4. def OAI.MetricKMedian.LPBinary.Repair.weights line 17
  5. def OAI.MetricKMedian.LPBinary.Repair.assignment line 18
  6. def OAI.MetricKMedian.LPBinary.Repair.assignments line 19
  7. def OAI.MetricKMedian.LPBinary.Repair.nearestRows line 20
  8. def OAI.MetricKMedian.LPBinary.Repair.finish line 21
  9. def OAI.MetricKMedian.LPBinary.Repair.raw line 23
  10. theorem OAI.MetricKMedian.LPBinary.Repair.opening_ofFn line 25
  11. theorem OAI.MetricKMedian.LPBinary.Repair.weights_ofFn line 29
  12. theorem OAI.MetricKMedian.LPBinary.Repair.assignments_ofFn line 32
  13. def OAI.MetricKMedian.LPBinary.Repair.encodeData line 38
  14. theorem OAI.MetricKMedian.LPBinary.Repair.raw_eq line 41
  15. def OAI.MetricKMedian.LPBinary.Repair.openingProgram line 63
  16. def OAI.MetricKMedian.LPBinary.Repair.weightsProgram line 69
  17. def OAI.MetricKMedian.LPBinary.Repair.assignmentProgram line 73
  18. def OAI.MetricKMedian.LPBinary.Repair.assignmentsProgram line 77
  19. def OAI.MetricKMedian.LPBinary.Repair.nearestRowsProgram line 79
  20. def OAI.MetricKMedian.LPBinary.Repair.lossProgram line 81
  21. def OAI.MetricKMedian.LPBinary.Repair.rawProgram line 83