OAI/Combinatorics/KMedian/Optimization/DualListOperations.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.LPBinary.maximum line 14
  2. theorem OAI.MetricKMedian.LPBinary.maximum_eq_finset line 16
  3. def OAI.MetricKMedian.LPBinary.Dual.candidates line 36
  4. def OAI.MetricKMedian.LPBinary.Dual.affine line 37
  5. def OAI.MetricKMedian.LPBinary.Dual.value line 38
  6. def OAI.MetricKMedian.LPBinary.Dual.best line 39
  7. def OAI.MetricKMedian.LPBinary.Dual.gradient line 41
  8. theorem OAI.MetricKMedian.LPBinary.Dual.affine_ofFn line 43
  9. theorem OAI.MetricKMedian.LPBinary.Dual.mem_candidates line 48
  10. theorem OAI.MetricKMedian.LPBinary.Dual.value_ofFn line 52
  11. theorem OAI.MetricKMedian.LPBinary.Dual.best_ofFn line 59
  12. theorem OAI.MetricKMedian.LPBinary.Dual.gradient_ofFn line 70