OAI/Combinatorics/KMedian/Optimization/LPBinaryStart.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.LPBinary.Context line 12
  2. abbrev OAI.MetricKMedian.LPBinary.ec line 13
  3. abbrev OAI.MetricKMedian.LPBinary.State line 14
  4. abbrev OAI.MetricKMedian.LPBinary.es line 15
  5. abbrev OAI.MetricKMedian.LPBinary.ei line 16
  6. def OAI.MetricKMedian.LPBinary.rawPenalty line 18
  7. def OAI.MetricKMedian.LPBinary.rawGrad line 19
  8. def OAI.MetricKMedian.LPBinary.rawRate line 20
  9. def OAI.MetricKMedian.LPBinary.rawSteps line 21
  10. def OAI.MetricKMedian.LPBinary.rawContext line 22
  11. def OAI.MetricKMedian.LPBinary.rawInitial line 23
  12. def OAI.MetricKMedian.LPBinary.start line 24
  13. def OAI.MetricKMedian.LPBinary.update line 25
  14. def OAI.MetricKMedian.LPBinary.Program.rawPenaltyProgram line 28
  15. def OAI.MetricKMedian.LPBinary.Program.rawGradProgram line 32
  16. def OAI.MetricKMedian.LPBinary.Program.rawRateProgram line 38
  17. def OAI.MetricKMedian.LPBinary.Program.rawStepsProgram line 42
  18. def OAI.MetricKMedian.LPBinary.Program.rawContextProgram line 47
  19. def OAI.MetricKMedian.LPBinary.Program.rawInitialProgram line 49
  20. def OAI.MetricKMedian.LPBinary.Program.inputRaw line 55
  21. def OAI.MetricKMedian.LPBinary.Program.startProgram line 57
  22. def OAI.MetricKMedian.LPBinary.Program.stepsProgram line 59
  23. def OAI.MetricKMedian.LPBinary.Program.updateProgram line 61
  24. theorem OAI.MetricKMedian.LPBinary.head_ofFn line 71
  25. theorem OAI.MetricKMedian.LPBinary.rawGrad_eq line 77
  26. theorem OAI.MetricKMedian.LPBinary.rawSteps_eq line 79
  27. theorem OAI.MetricKMedian.LPBinary.rawRate_eq line 83
  28. theorem OAI.MetricKMedian.LPBinary.start_eq line 86
  29. theorem OAI.MetricKMedian.LPBinary.update_eq line 95
  30. theorem OAI.MetricKMedian.LPBinary.update_iterate line 107