OAI/Combinatorics/KMedian/Optimization/SimplexListProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.LPBinary.upper line 15
  2. def OAI.MetricKMedian.LPBinary.threshold line 16
  3. def OAI.MetricKMedian.LPBinary.thresholds line 17
  4. def OAI.MetricKMedian.LPBinary.level line 18
  5. def OAI.MetricKMedian.LPBinary.project line 21
  6. theorem OAI.MetricKMedian.LPBinary.threshold_ofFn line 23
  7. theorem OAI.MetricKMedian.LPBinary.thresholds_ofFn line 27
  8. theorem OAI.MetricKMedian.LPBinary.level_ofFn line 34
  9. theorem OAI.MetricKMedian.LPBinary.project_ofFn line 58
  10. abbrev OAI.MetricKMedian.LPBinary.Program.ethreshold line 65
  11. def OAI.MetricKMedian.LPBinary.Program.upperProgram line 66
  12. def OAI.MetricKMedian.LPBinary.Program.thresholdProgram line 68
  13. def OAI.MetricKMedian.LPBinary.Program.thresholdsProgram line 77
  14. def OAI.MetricKMedian.LPBinary.Program.levelProgram line 80
  15. def OAI.MetricKMedian.LPBinary.Program.positivePart line 82
  16. def OAI.MetricKMedian.LPBinary.Program.projectProgram line 84