OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialCoefficientContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Coefficients of a continuous bounded-degree polynomial family

Each coefficient is a fixed finite linear combination of evaluations on the finite-dimensional space of bounded-degree polynomials. This supplies uniform coefficient bounds from compact parameter sets, even when the input cubes have growing radii.

  1. def OAI.PolycyclicRecognition.boundedDegreeEvaluation line 21
  2. theorem OAI.PolycyclicRecognition.boundedDegreeCoefficient_mem_span_evaluations line 25
  3. theorem OAI.PolycyclicRecognition.continuous_polynomial_coefficients line 39