OAI/Combinatorics/KMedianRecovery/Refined/Routes.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Reference-distance routes, endpoint partitions, covered centers, and the total radius bound.

  1. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.finalReference_le_first line 12
  2. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.finalInternal_subset line 16
  3. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.firstInternal_clients line 20
  4. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.finalInternal_clients line 24
  5. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.large_subset line 29
  6. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.small_subset line 30
  7. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.remaining_subset line 31
  8. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.firstRemaining_subset line 32
  9. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.sum_partition line 34
  10. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.remaining_sum line 48
  11. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.firstRemaining_sum line 54
  12. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.covered_subset line 61
  13. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.covered_nonempty line 64
  14. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.covered_disjoint line 67
  15. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.first_nonneg line 72
  16. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.final_nonneg line 76
  17. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.firstMass_nonneg line 84
  18. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.internal_bound line 87
  19. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.proxy_available line 93
  20. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.reference_proxy line 100
  21. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.leaf_route line 105
  22. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.first_near_route line 121
  23. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.fraction_nonneg line 137
  24. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.fraction_le_one line 141
  25. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.fraction_count line 149
  26. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.fraction_lt_third line 153
  27. lemma OAI.MetricKMedianRecovery.RefinedRecovery.EndpointData.radius_total line 163