OAI/Combinatorics/KMedian/Optimization/SimplexProjection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Simplex.upper line 11
  2. theorem OAI.MetricKMedian.Simplex.mem_upper_self line 14
  3. theorem OAI.MetricKMedian.Simplex.upper_card_pos line 17
  4. def OAI.MetricKMedian.Simplex.threshold line 20
  5. def OAI.MetricKMedian.Simplex.level line 23
  6. def OAI.MetricKMedian.Simplex.project line 26
  7. theorem OAI.MetricKMedian.Simplex.threshold_le_level line 28
  8. theorem OAI.MetricKMedian.Simplex.level_attained line 32
  9. theorem OAI.MetricKMedian.Simplex.threshold_sum line 38
  10. theorem OAI.MetricKMedian.Simplex.project_nonneg line 45
  11. theorem OAI.MetricKMedian.Simplex.project_sum line 47
  12. theorem OAI.MetricKMedian.Simplex.project_variational line 96
  13. theorem OAI.MetricKMedian.Simplex.project_sqdist line 120