OAI/Combinatorics/SumProduct/Alignment/AllLevel05.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AllLevelRemovals.Removal.smooth line 33
  2. lemma OAI.AllLevelRemovals.Removal.smooth_integer line 37
  3. def OAI.AllLevelRemovals.smoothWord line 49
  4. lemma OAI.AllLevelRemovals.smoothWord_integer line 51
  5. def OAI.AllLevelRemovals.scalarProfile line 58
  6. def OAI.AllLevelRemovals.profile line 62
  7. def OAI.AllLevelRemovals.parameters line 65
  8. def OAI.AllLevelRemovals.limitParameters line 69
  9. lemma OAI.AllLevelRemovals.parameters_tendsto line 74
  10. lemma OAI.AllLevelRemovals.scalarProfile_parameters line 83
  11. lemma OAI.AllLevelRemovals.scalarProfile_limit line 90
  12. lemma OAI.AllLevelRemovals.scalarProfile_polynomial line 96
  13. lemma OAI.AllLevelRemovals.polynomial_mul line 104
  14. lemma OAI.AllLevelRemovals.profile_polynomial line 117
  15. lemma OAI.AllLevelRemovals.profile_smooth line 138
  16. def OAI.AllLevelRemovals.smoothLimit line 149
  17. lemma OAI.AllLevelRemovals.smoothWord_eq_profile line 152
  18. theorem OAI.AllLevelRemovals.smoothWord_limit line 162
  19. theorem OAI.AllLevelRemovals.smoothWord_bounds line 173
  20. def OAI.AllLevelRemovals.prefixProfile line 202
  21. lemma OAI.AllLevelRemovals.prefixProfile_polynomial line 205
  22. def OAI.AllLevelRemovals.prefixParameters line 214
  23. def OAI.AllLevelRemovals.prefixLimitParameters line 216
  24. lemma OAI.AllLevelRemovals.prefixParameters_tendsto line 219
  25. lemma OAI.AllLevelRemovals.prefixProfile_parameters line 229
  26. lemma OAI.AllLevelRemovals.prefixProfile_limit line 233
  27. theorem OAI.AllLevelRemovals.prefix_smoothWord_limit line 237
  28. theorem OAI.AllLevelRemovals.prefix_smoothWord_bounds line 249
  29. theorem OAI.AllLevelRemovals.prefix_smoothLimit_smooth line 261