OAI/Combinatorics/KMedian/Optimization/FractionalDual.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.FractionalDual.affine line 12
  2. theorem OAI.MetricKMedian.FractionalDual.weak_duality line 14
  3. theorem OAI.MetricKMedian.FractionalDual.ordered_attains line 28
  4. def OAI.MetricKMedian.FractionalDual.thresholds line 62
  5. def OAI.MetricKMedian.FractionalDual.value line 64
  6. theorem OAI.MetricKMedian.FractionalDual.affine_le_value line 68
  7. theorem OAI.MetricKMedian.FractionalDual.value_le_assignment line 72
  8. theorem OAI.MetricKMedian.FractionalDual.value_attained line 80
  9. def OAI.MetricKMedian.FractionalDual.bestThreshold line 92
  10. theorem OAI.MetricKMedian.FractionalDual.bestThreshold_spec line 96
  11. def OAI.MetricKMedian.FractionalDual.gradient line 106
  12. theorem OAI.MetricKMedian.FractionalDual.gradient_spec line 109
  13. theorem OAI.MetricKMedian.FractionalDual.gradient_bound line 125