OAI/Combinatorics/KMedianRecovery/Recovery/Cluster.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Sampling.cluster line 10
  2. def OAI.MetricKMedianRecovery.Sampling.clusterCost line 13
  3. def OAI.MetricKMedianRecovery.Sampling.clusterMean line 16
  4. def OAI.MetricKMedianRecovery.Sampling.comparisonCost line 19
  5. lemma OAI.MetricKMedianRecovery.Sampling.cluster_mem line 23
  6. lemma OAI.MetricKMedianRecovery.Sampling.cluster_subset line 27
  7. lemma OAI.MetricKMedianRecovery.Sampling.cluster_partition line 31
  8. lemma OAI.MetricKMedianRecovery.Sampling.clusterCost_nonneg line 41
  9. lemma OAI.MetricKMedianRecovery.Sampling.clusterMean_nonneg line 44
  10. lemma OAI.MetricKMedianRecovery.Sampling.clusterMean_mul_card line 47
  11. lemma OAI.MetricKMedianRecovery.Sampling.comparisonCost_eq line 54
  12. structure OAI.MetricKMedianRecovery.Sampling.Comparison line 64
  13. def OAI.MetricKMedianRecovery.Sampling.Comparison.bad line 79
  14. def OAI.MetricKMedianRecovery.Sampling.Comparison.nonproxy line 80
  15. def OAI.MetricKMedianRecovery.Sampling.Comparison.covered line 81
  16. def OAI.MetricKMedianRecovery.Sampling.Comparison.near line 83
  17. def OAI.MetricKMedianRecovery.Sampling.Comparison.nearTotal line 85
  18. def OAI.MetricKMedianRecovery.Sampling.Comparison.removalTotal line 87
  19. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.nonproxy_card line 91
  20. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.proxy_survives line 97
  21. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.good_reference_bound line 104
  22. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_empty line 116
  23. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_add line 119
  24. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_remove line 123
  25. def OAI.MetricKMedianRecovery.Sampling.Comparison.Correct line 126
  26. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_initial line 136
  27. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_covered_subset line 140
  28. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_lengths line 146
  29. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_radii_nonneg line 157
  30. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_remove line 162
  31. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_add line 168
  32. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_witness line 193
  33. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.reference_leaf_mem line 197
  34. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_client_bound line 202
  35. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_cluster_bound line 211
  36. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.uncovered_cluster_bound line 262
  37. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.center_sum_partition line 310
  38. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_cost_aggregate line 319
  39. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_weight_bound line 338
  40. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.comparison_triangle line 365
  41. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_leaf_dominates line 369
  42. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_nearestLeaf_lower line 377