OAI/Combinatorics/KMedianRecovery/Recovery/Pool.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.PhaseMergePath.pool line 10
  2. lemma OAI.MetricKMedianRecovery.PhaseMergePath.subset_pool line 13
  3. lemma OAI.MetricKMedianRecovery.PhaseMergePath.insert_subset_pool line 17
  4. def OAI.MetricKMedianRecovery.PhaseMergePath.Good line 22
  5. inductive OAI.MetricKMedianRecovery.PhaseMergePath.Step line 26
  6. inductive OAI.MetricKMedianRecovery.PhaseMergePath.Walk line 37
  7. lemma OAI.MetricKMedianRecovery.PhaseMergePath.Walk.trans line 46
  8. lemma OAI.MetricKMedianRecovery.PhaseMergePath.Walk.first_good line 54
  9. lemma OAI.MetricKMedianRecovery.PhaseMergePath.Walk.last_good line 61
  10. lemma OAI.MetricKMedianRecovery.PhaseMergePath.regular_good line 68
  11. lemma OAI.MetricKMedianRecovery.PhaseMergePath.one_copy_good line 75
  12. theorem OAI.MetricKMedianRecovery.PhaseMergePath.delete_old_suffix line 87
  13. lemma OAI.MetricKMedianRecovery.PhaseMergePath.regular_length line 150
  14. theorem OAI.MetricKMedianRecovery.PhaseMergePath.advance_prefix line 155
  15. theorem OAI.MetricKMedianRecovery.PhaseMergePath.match_prefix line 207
  16. theorem OAI.MetricKMedianRecovery.PhaseMergePath.prune_suffix line 260
  17. theorem OAI.MetricKMedianRecovery.PhaseMergePath.regular_phase_path line 296