OAI/GroupTheory/PolycyclicRecognition/Geometry/PolynomialDerivativeGrowth.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Derivative bounds on growing polynomial input cubes

  1. theorem OAI.PolycyclicRecognition.continuous_pderiv_evaluation line 15
  2. theorem OAI.PolycyclicRecognition.norm_clm_pi_domain_le line 26
  3. def OAI.PolycyclicRecognition.polynomialMapDifferential line 44
  4. theorem OAI.PolycyclicRecognition.hasFDerivAt_polynomialMap line 48
  5. theorem OAI.PolycyclicRecognition.polynomialMapDifferential_basis line 53
  6. theorem OAI.PolycyclicRecognition.norm_polynomialMapDifferential_le line 58
  7. theorem OAI.PolycyclicRecognition.norm_polynomialDifferential_le line 68
  8. theorem OAI.PolycyclicRecognition.uniform_polynomial_map_derivative_bounds line 76