OAI/Combinatorics/KMedianRecovery/Recovery/NearEligible.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.correct_entry_exists line 12
  2. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.third_ball_disjoint line 67
  3. def OAI.MetricKMedianRecovery.Sampling.Comparison.nearEligible line 91
  4. def OAI.MetricKMedianRecovery.Sampling.Comparison.removalEligible line 95
  5. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.nearTotal_eq line 98
  6. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.nearTotal_nonneg line 119
  7. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.removalTotal_nonneg line 125
  8. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.nearTotal_le_weight line 130
  9. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.removalTotal_le_weight line 142
  10. def OAI.MetricKMedianRecovery.Sampling.Comparison.Terminal line 152
  11. def OAI.MetricKMedianRecovery.Sampling.Comparison.counter line 156
  12. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.counter_zero_terminal line 159
  13. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.eligible_ball_correct line 176
  14. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.counter_ball_decreases line 187
  15. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.counter_remove_decreases line 195
  16. def OAI.MetricKMedianRecovery.Sampling.Comparison.conditionalClients line 210
  17. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.conditionalClients_pos line 230
  18. def OAI.MetricKMedianRecovery.Sampling.Comparison.mainKappa line 243
  19. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.mainKappa_pos line 244
  20. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.mainKappa_le_one line 245
  21. abbrev OAI.MetricKMedianRecovery.Sampling.Comparison.MainEntry line 246
  22. abbrev OAI.MetricKMedianRecovery.Sampling.Comparison.MainAction line 248
  23. def OAI.MetricKMedianRecovery.Sampling.Comparison.prescribedEntry line 251
  24. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.prescribedEntry_spec line 258
  25. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.eligible_near_weight line 276
  26. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.eligible_removal_weight line 283
  27. def OAI.MetricKMedianRecovery.Sampling.Comparison.activeGuide line 289
  28. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.activeGuide_support line 309
  29. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.active_weight_pos line 330
  30. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.update_eligible_ball line 342
  31. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.update_eligible_removal line 359
  32. abbrev OAI.MetricKMedianRecovery.Sampling.Comparison.mainActual line 373
  33. def OAI.MetricKMedianRecovery.Sampling.Comparison.stop line 377