OAI/Combinatorics/SumProduct/Alignment/MalcevTail02.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MalcevTailFactor.beta line 30
  2. def OAI.MalcevTailFactor.numerator line 32
  3. def OAI.MalcevTailFactor.error line 34
  4. def OAI.MalcevTailFactor.smallCoeff line 36
  5. def OAI.MalcevTailFactor.rationalGenerator line 38
  6. def OAI.MalcevTailFactor.rationalCoeff line 40
  7. lemma OAI.MalcevTailFactor.beta_zero line 44
  8. lemma OAI.MalcevTailFactor.error_zero line 49
  9. lemma OAI.MalcevTailFactor.rationalCoeff_eq line 53
  10. lemma OAI.MalcevTailFactor.small_character line 59
  11. lemma OAI.MalcevTailFactor.rational_character line 65
  12. lemma OAI.MalcevTailFactor.generator_rational line 72
  13. lemma OAI.MalcevTailFactor.small_bound line 75
  14. lemma OAI.MalcevTailFactor.word_character_split line 82
  15. lemma OAI.MalcevTailFactor.residual_kernel line 94
  16. lemma OAI.MalcevTailFactor.small_polynomial line 106
  17. lemma OAI.MalcevTailFactor.rational_polynomial line 113
  18. theorem OAI.CubePolynomials.residual_refinement line 134
  19. theorem OAI.RationalFactorPeriods.uniform_rational_word_period line 175
  20. def OAI.CharacterFactorization.epsilon line 232
  21. def OAI.CharacterFactorization.gamma line 235
  22. def OAI.CharacterFactorization.residual line 238
  23. lemma OAI.CharacterFactorization.factorization_identity line 241
  24. lemma OAI.CharacterFactorization.epsilon_polynomial line 247
  25. lemma OAI.CharacterFactorization.gamma_polynomial line 259
  26. lemma OAI.CharacterFactorization.epsilon_zero line 270
  27. lemma OAI.CharacterFactorization.residual_polynomial line 277
  28. theorem OAI.CharacterFactorization.normalized_factorization line 294
  29. theorem OAI.CharacterFactorization.uniform_gamma_period line 311