OAI/Combinatorics/KMedianRecovery/Recovery/Score.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Completion.score line 9
  2. lemma OAI.MetricKMedianRecovery.Completion.score_le_iff line 12
  3. lemma OAI.MetricKMedianRecovery.Completion.le_score_iff line 16
  4. lemma OAI.MetricKMedianRecovery.Completion.score_empty line 20
  5. lemma OAI.MetricKMedianRecovery.Completion.baseline_le_score line 23
  6. lemma OAI.MetricKMedianRecovery.Completion.offer_le_score line 26
  7. lemma OAI.MetricKMedianRecovery.Completion.score_mono line 30
  8. lemma OAI.MetricKMedianRecovery.Completion.score_insert line 34
  9. lemma OAI.MetricKMedianRecovery.Completion.score_diminishing line 46
  10. def OAI.MetricKMedianRecovery.Completion.topSum line 59
  11. lemma OAI.MetricKMedianRecovery.Completion.le_topSum line 63
  12. lemma OAI.MetricKMedianRecovery.Completion.topSum_le line 69
  13. lemma OAI.MetricKMedianRecovery.Completion.topSum_attained line 76
  14. lemma OAI.MetricKMedianRecovery.Completion.topSum_mono line 86
  15. lemma OAI.MetricKMedianRecovery.Completion.topSum_exchange line 92
  16. lemma OAI.MetricKMedianRecovery.Completion.topScores_diminishing line 168
  17. def OAI.MetricKMedianRecovery.Completion.bottomSum line 195
  18. lemma OAI.MetricKMedianRecovery.Completion.bottomSum_attained line 197
  19. lemma OAI.MetricKMedianRecovery.Completion.bottomSum_le line 204
  20. def OAI.MetricKMedianRecovery.Completion.cappedCost line 210
  21. lemma OAI.MetricKMedianRecovery.Completion.cappedCost_empty line 213
  22. lemma OAI.MetricKMedianRecovery.Completion.complement_cappedCost line 216
  23. def OAI.MetricKMedianRecovery.Completion.surrogate line 230
  24. def OAI.MetricKMedianRecovery.Completion.saving line 236
  25. lemma OAI.MetricKMedianRecovery.Completion.saving_eq_scores line 242
  26. lemma OAI.MetricKMedianRecovery.Completion.saving_empty line 259
  27. lemma OAI.MetricKMedianRecovery.Completion.saving_mono line 264
  28. lemma OAI.MetricKMedianRecovery.Completion.saving_nonneg line 277
  29. lemma OAI.MetricKMedianRecovery.Completion.saving_diminishing line 285