OAI/Combinatorics/KMedianRecovery/Refined/Clusters.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Nearest-center clusters, integral metric costs, certificate cardinalities, and precision estimates.

  1. def OAI.MetricKMedianRecovery.RefinedRecovery.Input.pointMetric line 12
  2. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.pointMetric_dist line 23
  3. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.pointMetric_clusterCost line 27
  4. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.size_eq_pointCount line 31
  5. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.assign_mem line 35
  6. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.assign_key_le line 41
  7. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.assign_nearest line 49
  8. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.cost_eq_assigned line 53
  9. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.cluster_mem line 62
  10. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.cluster_subset line 65
  11. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.cluster_partition line 68
  12. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.sum_clusterCost line 77
  13. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.cost_nonneg line 89
  14. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.separated line 95
  15. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Input.integer_cost line 105
  16. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.centers_nonempty line 132
  17. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.clients_nonempty line 137
  18. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.size_ge_two line 145
  19. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.nonproxy_card line 151
  20. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.bad_card_le line 157
  21. theorem OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.zero_bad_anchor line 161
  22. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Certificate.zero_bad_target line 185
  23. lemma OAI.MetricKMedianRecovery.RefinedRecovery.precision_lt line 196
  24. lemma OAI.MetricKMedianRecovery.RefinedRecovery.precision_error_le line 203