OAI/Combinatorics/KMedian/Optimization/FractionalListChecks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.LPBinary.Repair.bounded line 14
  2. def OAI.MetricKMedian.LPBinary.Repair.dominated line 15
  3. def OAI.MetricKMedian.LPBinary.Repair.valid line 16
  4. def OAI.MetricKMedian.LPBinary.Repair.dot line 19
  5. def OAI.MetricKMedian.LPBinary.Repair.value line 20
  6. theorem OAI.MetricKMedian.LPBinary.Repair.all_ofFn line 22
  7. theorem OAI.MetricKMedian.LPBinary.Repair.valid_encodeData line 26
  8. theorem OAI.MetricKMedian.LPBinary.Repair.value_encodeData line 34
  9. def OAI.MetricKMedian.LPBinary.Repair.boundedProgram line 39
  10. def OAI.MetricKMedian.LPBinary.Repair.dominatedProgram line 43
  11. def OAI.MetricKMedian.LPBinary.Repair.validProgram line 47
  12. def OAI.MetricKMedian.LPBinary.Repair.dotProgram line 59
  13. def OAI.MetricKMedian.LPBinary.Repair.valueProgram line 61