OAI/Combinatorics/EditDistance/Histograms.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Hash separation and finite histogram inequalities

  1. def OAI.EditCutHash.hit line 17
  2. lemma OAI.EditCutHash.hit_nonneg line 19
  3. lemma OAI.EditCutHash.hit_le_one line 21
  4. lemma OAI.EditCutHash.hit_self line 23
  5. def OAI.EditCutHash.count line 25
  6. def OAI.EditCutHash.histogramDistance line 26
  7. lemma OAI.EditCutHash.count_nonneg line 29
  8. lemma OAI.EditCutHash.histogramDistance_nonneg line 30
  9. lemma OAI.EditCutHash.hit_sum line 33
  10. lemma OAI.EditCutHash.count_sum line 37
  11. lemma OAI.EditCutHash.hit_distance line 42
  12. lemma OAI.EditCutHash.histogramDistance_le line 59
  13. lemma OAI.EditCutHash.histogramDistance_disjoint line 70
  14. lemma OAI.EditCutHash.histogramDistance_lower line 94