OAI/Combinatorics/KMedianRecovery/Geometry/ClusterCost.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Surplus.clusterCost line 11
  2. def OAI.MetricKMedianRecovery.Surplus.partCost line 13
  3. def OAI.MetricKMedianRecovery.Surplus.partCharge line 15
  4. lemma OAI.MetricKMedianRecovery.Surplus.cluster_sum line 19
  5. lemma OAI.MetricKMedianRecovery.Surplus.clusterCost_nonneg line 32
  6. lemma OAI.MetricKMedianRecovery.Surplus.partCost_nonneg line 34
  7. lemma OAI.MetricKMedianRecovery.Surplus.total_cluster_cost line 37
  8. lemma OAI.MetricKMedianRecovery.Surplus.partition_cost line 47
  9. lemma OAI.MetricKMedianRecovery.Surplus.protected_partition_cost line 53
  10. lemma OAI.MetricKMedianRecovery.Surplus.cluster_dual_bound line 95
  11. lemma OAI.MetricKMedianRecovery.Surplus.any_solution_dual line 107