OAI/Combinatorics/KMedianRecovery/Recovery/Destination.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.Completion.convex_surrogate_upper line 8
  2. lemma OAI.MetricKMedianRecovery.Completion.cappedCost_le_base line 38
  3. lemma OAI.MetricKMedianRecovery.Completion.cappedCost_le_offer line 41
  4. lemma OAI.MetricKMedianRecovery.Completion.virtualNearest_le_real line 47
  5. lemma OAI.MetricKMedianRecovery.Completion.virtualNearest_le_ball line 52
  6. inductive OAI.MetricKMedianRecovery.Completion.Destination line 57
  7. def OAI.MetricKMedianRecovery.Completion.mixedDistance line 63
  8. lemma OAI.MetricKMedianRecovery.Completion.mixedDistance_covered_triangle line 71
  9. lemma OAI.MetricKMedianRecovery.Completion.red_mixed_comparison line 87
  10. def OAI.MetricKMedianRecovery.Completion.assignedClients line 114
  11. lemma OAI.MetricKMedianRecovery.Completion.weighted_removal_bound line 119
  12. lemma OAI.MetricKMedianRecovery.Completion.interpolated_client_sum line 149