OAI/Combinatorics/KMedianRecovery/Recovery/CoveredCenter.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Sampling.Comparison.coveredCenter line 10
  2. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.coveredCenter_mem line 12
  3. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.exists_coveredCenter line 16
  4. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.coveredCenter_injective line 22
  5. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.covered_card_eq_length line 33
  6. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.coveredCenter_ball line 37
  7. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.coveredCenter_facility line 41
  8. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.leaderPair_eq_indexed line 46
  9. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.exact_completion_counts line 52
  10. def OAI.MetricKMedianRecovery.Sampling.Comparison.coveredIndex line 62
  11. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.coveredIndex_spec line 65
  12. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.leafPair_index line 68
  13. def OAI.MetricKMedianRecovery.Sampling.leafCenter line 79
  14. def OAI.MetricKMedianRecovery.Sampling.leafRadius line 80
  15. def OAI.MetricKMedianRecovery.Sampling.toVirtual line 82
  16. lemma OAI.MetricKMedianRecovery.Sampling.toVirtual_real_iff line 89
  17. lemma OAI.MetricKMedianRecovery.Sampling.toVirtual_mem line 104
  18. lemma OAI.MetricKMedianRecovery.Sampling.toVirtual_distance line 116
  19. lemma OAI.MetricKMedianRecovery.Sampling.reference_eq_virtualNearest line 130
  20. def OAI.MetricKMedianRecovery.Sampling.completionAssignment line 146
  21. lemma OAI.MetricKMedianRecovery.Sampling.completionAssignment_mem line 149
  22. lemma OAI.MetricKMedianRecovery.Sampling.completionAssignment_distance line 153
  23. lemma OAI.MetricKMedianRecovery.Sampling.completionAssignment_real_iff line 159
  24. lemma OAI.MetricKMedianRecovery.Sampling.assigned_clients_agree line 163
  25. lemma OAI.MetricKMedianRecovery.Sampling.assigned_reference_total_agree line 169