OAI/Combinatorics/EditDistance/LowerParameters.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Recursive parameter bounds and exponential lower scales

  1. def OAI.EditParameters.b line 13
  2. def OAI.EditParameters.P line 14
  3. def OAI.EditParameters.h line 15
  4. def OAI.EditParameters.eta line 16
  5. lemma OAI.EditParameters.prime_parameter_pos line 18
  6. lemma OAI.EditParameters.eta_numerator_bound line 22
  7. lemma OAI.EditParameters.eta_le line 39
  8. lemma OAI.EditParameters.budget_bound line 48
  9. theorem OAI.EditParameters.budget_small line 65
  10. def OAI.EditParameters.codeBits line 72
  11. def OAI.EditParameters.codeWidth line 73
  12. def OAI.EditParameters.encodedLength line 74
  13. lemma OAI.EditParameters.alphabet_power_bound line 76
  14. lemma OAI.EditParameters.bits_poly line 97
  15. lemma OAI.EditParameters.width_poly line 100
  16. lemma OAI.EditParameters.width_pos line 105
  17. lemma OAI.EditParameters.encodedLength_pos line 106
  18. lemma OAI.EditParameters.length_power_bound line 109
  19. theorem OAI.EditParameters.log_length_bound line 124
  20. def OAI.EditParameters.lowerRatio line 176
  21. lemma OAI.EditParameters.log_width_le line 178
  22. theorem OAI.EditParameters.ratio_exponential line 188