OAI/Combinatorics/KMedianRecovery/Refined/Charges.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Near-client mass, population radii, and the five classes of cluster charge.

  1. def OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.q line 11
  2. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.q_pos line 13
  3. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.q_eq line 16
  4. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.near_bound line 21
  5. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.radius_sum line 30
  6. def OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.baseCharge line 63
  7. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.baseCharge_le_base line 66
  8. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.baseCharge_le_offer line 73
  9. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.baseCharge_le_center line 79
  10. def OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.clusterCharge line 88
  11. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.clusterCharge_le line 91
  12. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.clusterCharge_eq line 100
  13. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.good_charge line 104
  14. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.first_covered line 112
  15. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.split_charge line 139
  16. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.second_coefficient line 151
  17. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.second_covered_precise line 156
  18. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.second_covered line 191
  19. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.clusterCharge_empty line 217
  20. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.intersection_fraction_mono line 220
  21. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.uncovered_large line 225
  22. lemma OAI.MetricKMedianRecovery.RefinedRecovery.Analysis.uncovered_small line 273