OAI/Combinatorics/EditDistance/CutModels.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Finite weighted cuts and histogram lifts

  1. def OAI.EditCutModel.sep line 17
  2. structure OAI.EditCutModel.Model line 19
  3. def OAI.EditCutModel.Model.dist line 28
  4. lemma OAI.EditCutModel.Model.dist_nonneg line 31
  5. lemma OAI.EditCutModel.Model.dist_self line 38
  6. lemma OAI.EditCutModel.Model.dist_symm line 41
  7. lemma OAI.EditCutModel.Model.dist_triangle line 47
  8. def OAI.EditCutModel.Model.pullback line 57
  9. lemma OAI.EditCutModel.Model.pullback_dist line 64
  10. def OAI.EditCutModel.Model.scale line 67
  11. lemma OAI.EditCutModel.Model.scale_dist line 74
  12. def OAI.EditCutModel.Model.total line 79
  13. lemma OAI.EditCutModel.Model.total_dist line 86
  14. lemma OAI.EditCutModel.initial_cut_sum line 92
  15. theorem OAI.EditCutModel.threshold_sum line 96
  16. def OAI.EditCutModel.countNat line 120
  17. lemma OAI.EditCutModel.count_cast line 123
  18. lemma OAI.EditCutModel.count_bound line 127
  19. def OAI.EditCutModel.Model.histogram line 130
  20. lemma OAI.EditCutModel.Model.histogram_dist line 138
  21. lemma OAI.EditCutModel.Model.distance_eq line 156