OAI/Combinatorics/KMedianRecovery/Recovery/Guide.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Sampling.Comparison.guideAt line 13
  2. def OAI.MetricKMedianRecovery.Sampling.Comparison.guideKernel line 25
  3. def OAI.MetricKMedianRecovery.Sampling.Comparison.stoppedActual line 32
  4. def OAI.MetricKMedianRecovery.Sampling.Comparison.guidedUpdate line 35
  5. def OAI.MetricKMedianRecovery.Sampling.Comparison.Valid line 41
  6. def OAI.MetricKMedianRecovery.Sampling.Comparison.remaining line 45
  7. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.guide_invariant line 49
  8. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.guide_counter_decreases line 75
  9. theorem OAI.MetricKMedianRecovery.Sampling.Comparison.guide_hits line 98
  10. def OAI.MetricKMedianRecovery.Sampling.Comparison.actionMenuWeight line 117
  11. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.actionMenuWeight_nonneg line 123
  12. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.weighted_ratio_bound line 130
  13. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.activeGuide_domination line 139
  14. def OAI.MetricKMedianRecovery.Sampling.Comparison.guideLoss line 192
  15. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.guideLoss_nonneg line 197
  16. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.guideLoss_domination line 206
  17. def OAI.MetricKMedianRecovery.Sampling.Comparison.history line 236
  18. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_state line 241
  19. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_correct line 258
  20. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.supported_guide_step line 271
  21. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_step line 303
  22. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_leaves_mono line 330
  23. def OAI.MetricKMedianRecovery.Sampling.Comparison.IsBall line 348
  24. def OAI.MetricKMedianRecovery.Sampling.Comparison.IsThird line 349
  25. def OAI.MetricKMedianRecovery.Sampling.Comparison.ballLeader line 351
  26. def OAI.MetricKMedianRecovery.Sampling.Comparison.ballSteps line 355
  27. def OAI.MetricKMedianRecovery.Sampling.Comparison.thirdSteps line 358
  28. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.thirdSteps_subset line 362
  29. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.history_ball line 368