OAI/Combinatorics/KMedianRecovery/Refined/ChargeBound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The refined bound for total comparison-cluster charge.

  1. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.lostCharge line 11
  2. def OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.nearExternalCharge line 14
  3. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.remaining_bad line 17
  4. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.remaining_not_covered line 20
  5. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.good_clusterCharge line 26
  6. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.good_charge_sum line 35
  7. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.first_clusterCharge line 39
  8. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.second_clusterCharge line 55
  9. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.large_clusterCharge line 74
  10. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.small_clusterCharge line 94
  11. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.lostCharge_bound line 113
  12. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.nearExternalCharge_bound line 123
  13. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.fraction_cost_bound line 130
  14. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.weighted_radius_bound line 136
  15. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.totalCharge_eq_completion line 148
  16. theorem OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.refined_charge_bound line 167
  17. theorem OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.refined_charge_bound_six_mu line 204