OAI/GroupTheory/PolycyclicRecognition/Analysis/BoxCoordinateChanges.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate changes between the individual and union boxes

The target normalization uses a maximizing word basis. Inclusion of the individual support costs gives a uniform bound on the coordinate change. When a letter attains the union support on one side, its two normalized vectors correspond exactly under this map.

  1. theorem OAI.PolycyclicRecognition.bracketWordExponent_mono line 21
  2. def OAI.PolycyclicRecognition.boxCoordinateChange line 26
  3. theorem OAI.PolycyclicRecognition.boxCoordinateChange_apply line 30
  4. theorem OAI.PolycyclicRecognition.boxCoordinateChange_coordinates line 34
  5. theorem OAI.PolycyclicRecognition.exists_uniform_boxCoordinateChange_bound line 39
  6. theorem OAI.PolycyclicRecognition.rescaled_generator_in_coordinate_image line 62