OAI/Combinatorics/KMedian/Optimization/LPBinaryTrajectory.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.LPBinary.statePolynomial line 14
  2. theorem OAI.MetricKMedian.LPBinary.state_size line 17
  3. def OAI.MetricKMedian.LPBinary.states line 33
  4. def OAI.MetricKMedian.LPBinary.trajectory line 34
  5. theorem OAI.MetricKMedian.LPBinary.states_eq line 36
  6. theorem OAI.MetricKMedian.LPBinary.trajectory_eq line 42
  7. def OAI.MetricKMedian.LPBinary.value line 47
  8. def OAI.MetricKMedian.LPBinary.choose line 48
  9. def OAI.MetricKMedian.LPBinary.result line 49
  10. def OAI.MetricKMedian.LPBinary.Program.statesProgram line 52
  11. def OAI.MetricKMedian.LPBinary.Program.trajectoryProgram line 57
  12. def OAI.MetricKMedian.LPBinary.Program.valueProgram line 59
  13. def OAI.MetricKMedian.LPBinary.Program.chooseProgram line 64
  14. def OAI.MetricKMedian.LPBinary.Program.optimizeProgram line 77
  15. theorem OAI.MetricKMedian.LPBinary.value_eq line 81
  16. theorem OAI.MetricKMedian.LPBinary.result_eq line 88