OAI/Combinatorics/KMedianRecovery/Recovery/MergeCross.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedianRecovery.PhaseMergeCompletion.exists_regular_history line 10
  2. theorem OAI.MetricKMedianRecovery.PhaseMergeCompletion.prefix_twin line 24
  3. lemma OAI.MetricKMedianRecovery.PhaseMergeCompletion.absent_after_prefix line 61
  4. lemma OAI.MetricKMedianRecovery.PhaseMergeCompletion.free_absent_after line 70
  5. theorem OAI.MetricKMedianRecovery.PhaseMergeCompletion.history_twin line 78
  6. theorem OAI.MetricKMedianRecovery.PhaseMergeCompletion.attains_exists line 108
  7. lemma OAI.MetricKMedianRecovery.PhaseMergeCompletion.attains_zero line 113
  8. theorem OAI.MetricKMedianRecovery.PhaseMergeCompletion.attains_twin line 119
  9. def OAI.MetricKMedianRecovery.PhaseCountCrossing.Sandwich line 137
  10. lemma OAI.MetricKMedianRecovery.PhaseCountCrossing.Sandwich.symm line 139
  11. inductive OAI.MetricKMedianRecovery.PhaseCountCrossing.LengthEdit line 141
  12. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.Runs line 153
  13. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.paid line 157
  14. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.finalCount line 159
  15. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.Runs.attains line 162
  16. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.continuation line 166
  17. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.continuation_spec line 170
  18. inductive OAI.MetricKMedianRecovery.CanonicalMergeCrossing.Result line 180
  19. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.Result.Correct line 185
  20. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.twin_replay line 199
  21. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.coincident_paid line 219
  22. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.coincident_length line 225
  23. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.forward line 237
  24. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.forward_reverse line 242
  25. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.freeAppend_paid line 256
  26. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.paidDelete_paid line 272
  27. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.edit_forward line 283
  28. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.directed line 302
  29. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.edge line 307
  30. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.directed_spec line 310
  31. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.edge_spec line 342
  32. instance OAI.MetricKMedianRecovery.CanonicalMergeCrossing.(instance at line 360) line 360
  33. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.scan line 362
  34. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.scan_spec line 371
  35. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.Runs.mono_free line 401
  36. lemma OAI.MetricKMedianRecovery.CanonicalMergeCrossing.disjoint_pool line 413
  37. def OAI.MetricKMedianRecovery.CanonicalMergeCrossing.regularCross line 422
  38. theorem OAI.MetricKMedianRecovery.CanonicalMergeCrossing.regularCross_spec line 429