OAI/GroupTheory/PolycyclicRecognition/Algebra/UniformPolynomialGrowth.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform polynomial growth over compact coefficient families

  1. theorem OAI.PolycyclicRecognition.finite_bounded_exponents line 13
  2. theorem OAI.PolycyclicRecognition.norm_monomial_value_le line 18
  3. theorem OAI.PolycyclicRecognition.polynomial_support_subset_bounded_exponents line 32
  4. theorem OAI.PolycyclicRecognition.continuous_polynomial_evaluation_of_coefficients line 40
  5. theorem OAI.PolycyclicRecognition.exists_uniform_polynomial_growth line 57
  6. theorem OAI.PolycyclicRecognition.exists_uniform_finite_polynomial_growth line 96