OAI/Combinatorics/EditDistance/DirectSums.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Weighted direct sums and normalized slice maps

  1. abbrev OAI.EditL1.L1 line 12
  2. abbrev OAI.EditL1.L1On line 13
  3. lemma OAI.EditL1.norm_eq_tsum line 15
  4. lemma OAI.EditL1.summable_abs line 18
  5. def OAI.EditL1.reindex line 21
  6. lemma OAI.EditL1.reindex_apply line 26
  7. lemma OAI.EditL1.reindex_norm line 29
  8. lemma OAI.EditL1.reindex_sub line 34
  9. lemma OAI.EditL1.family_summable line 42
  10. def OAI.EditL1.familyLp line 46
  11. lemma OAI.EditL1.familyLp_apply line 49
  12. lemma OAI.EditL1.familyLp_norm line 51
  13. lemma OAI.EditL1.familyLp_sub line 57
  14. def OAI.EditL1.indexEquiv line 63
  15. def OAI.EditL1.pack line 65
  16. lemma OAI.EditL1.pack_norm line 67
  17. lemma OAI.EditL1.pack_sub line 70
  18. lemma OAI.EditL1.pack_distance line 74
  19. lemma OAI.EditL1.weighted_pack_distance line 78
  20. lemma OAI.EditAverage.avg_prod line 90
  21. lemma OAI.EditSlices.split_add_single line 105
  22. def OAI.EditSlices.slice line 114
  23. lemma OAI.EditSlices.variation_slice line 119