OAI/Combinatorics/KMedianRecovery/Recovery/Chosen.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.ShortSelection.product_event line 8
  2. lemma OAI.MetricKMedianRecovery.ShortSelection.pair_probability line 19
  3. def OAI.MetricKMedianRecovery.ShortSelection.chosen line 43
  4. lemma OAI.MetricKMedianRecovery.ShortSelection.uniform_total line 46
  5. lemma OAI.MetricKMedianRecovery.ShortSelection.mean_chosen line 52
  6. theorem OAI.MetricKMedianRecovery.ShortSelection.exists_simultaneous line 67
  7. lemma OAI.MetricKMedianRecovery.Anchoring.erase_nonempty_of_two line 94
  8. def OAI.MetricKMedianRecovery.Anchoring.neighbor line 102
  9. lemma OAI.MetricKMedianRecovery.Anchoring.neighbor_mem line 104
  10. lemma OAI.MetricKMedianRecovery.Anchoring.neighbor_ne line 106
  11. lemma OAI.MetricKMedianRecovery.Anchoring.neighbor_dist line 108
  12. lemma OAI.MetricKMedianRecovery.Anchoring.remaining_nonempty line 112
  13. lemma OAI.MetricKMedianRecovery.Anchoring.removal_routing_bound line 119
  14. theorem OAI.MetricKMedianRecovery.Anchoring.short_removal line 156