OAI/Combinatorics/KMedianRecovery/Recovery/State2.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedianRecovery.Sampling.State line 7
  2. def OAI.MetricKMedianRecovery.Sampling.State.initial line 13
  3. def OAI.MetricKMedianRecovery.Sampling.State.remove line 14
  4. def OAI.MetricKMedianRecovery.Sampling.State.add line 17
  5. abbrev OAI.MetricKMedianRecovery.Sampling.Tag line 22
  6. def OAI.MetricKMedianRecovery.Sampling.realTag line 24
  7. def OAI.MetricKMedianRecovery.Sampling.leafTag line 25
  8. def OAI.MetricKMedianRecovery.Sampling.tags line 27
  9. lemma OAI.MetricKMedianRecovery.Sampling.tags_nonempty line 31
  10. lemma OAI.MetricKMedianRecovery.Sampling.real_mem_tags line 36
  11. lemma OAI.MetricKMedianRecovery.Sampling.leaf_mem_tags line 41
  12. def OAI.MetricKMedianRecovery.Sampling.tagDistance line 45
  13. def OAI.MetricKMedianRecovery.Sampling.chosen line 53
  14. lemma OAI.MetricKMedianRecovery.Sampling.chosen_mem line 57
  15. lemma OAI.MetricKMedianRecovery.Sampling.chosen_key_le line 62
  16. def OAI.MetricKMedianRecovery.Sampling.reference line 69
  17. lemma OAI.MetricKMedianRecovery.Sampling.reference_le line 72
  18. lemma OAI.MetricKMedianRecovery.Sampling.reference_le_real line 76
  19. lemma OAI.MetricKMedianRecovery.Sampling.reference_le_diameter line 80
  20. lemma OAI.MetricKMedianRecovery.Sampling.reference_le_leaf line 84
  21. lemma OAI.MetricKMedianRecovery.Sampling.tagDistance_triangle line 92
  22. lemma OAI.MetricKMedianRecovery.Sampling.reference_triangle line 106
  23. lemma OAI.MetricKMedianRecovery.Sampling.reference_nonneg line 111
  24. lemma OAI.MetricKMedianRecovery.Sampling.tags_add_mono line 128
  25. lemma OAI.MetricKMedianRecovery.Sampling.tagDistance_add_old line 134
  26. lemma OAI.MetricKMedianRecovery.Sampling.reference_add_le line 148
  27. lemma OAI.MetricKMedianRecovery.Sampling.chosen_add_consistent line 153