OAI/Combinatorics/EditDistance/BinaryEmbedding.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Fixed-length binary embeddings with unrestricted edit distance

  1. lemma OAI.EditDistortion.Script.flatMap line 12
  2. lemma OAI.EditDistortion.indel_flatMap_le line 29
  3. lemma OAI.EditDistortion.indel_replicate_le line 33
  4. theorem OAI.EditCode.indel_code_upper line 50
  5. def OAI.EditCode.fixed line 54
  6. lemma OAI.EditCode.fixed_length line 57
  7. theorem OAI.EditCode.indel_fixed_upper line 61
  8. def OAI.EditCode.labels line 85