OAI/Combinatorics/KMedian/Optimization/TruncatedObjective.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.TruncatedLP.truncated line 12
  2. theorem OAI.MetricKMedian.TruncatedLP.truncated_bounds line 16
  3. def OAI.MetricKMedian.TruncatedLP.objective line 24
  4. def OAI.MetricKMedian.TruncatedLP.gradient line 27
  5. theorem OAI.MetricKMedian.TruncatedLP.subgradient line 30
  6. theorem OAI.MetricKMedian.TruncatedLP.gradient_abs_bound line 39
  7. theorem OAI.MetricKMedian.TruncatedLP.gradient_sq_bound line 49
  8. theorem OAI.MetricKMedian.TruncatedLP.objective_le_assignment line 59
  9. theorem OAI.MetricKMedian.TruncatedLP.objective_attained line 64