OAI/Combinatorics/EditDistance/LowerDistortion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Distortion lower bounds from separated finite word families

  1. def OAI.EditLower.codeWord line 17
  2. def OAI.EditLower.codeSet line 18
  3. def OAI.EditLower.codePoint line 19
  4. lemma OAI.EditLower.codeSet_finite line 21
  5. lemma OAI.EditLower.codeSet_nonempty line 22
  6. lemma OAI.EditLower.codeSet_length line 23
  7. lemma OAI.EditLower.far_after_code line 27
  8. lemma OAI.EditLower.codeSet_nontrivial line 41
  9. theorem OAI.EditLower.family_distortion line 50