OAI/Combinatorics/EditDistance/UpperRecursion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-cut embeddings at recursive capacities

  1. lemma OAI.EditUpperParameters.log_two_bounds line 12
  2. lemma OAI.EditUpperParameters.scale_count_bound line 21
  3. lemma OAI.EditUpperParameters.log_square_bound line 33
  4. lemma OAI.EditUpperParameters.step_constant_bound line 41
  5. def OAI.EditUpper.growth line 73
  6. lemma OAI.EditUpper.growth_ge line 75
  7. theorem OAI.EditUpper.exists_level line 81