OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCoverWordBoxes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential box bounds for all compact words in the cover

Bounded Cartan increments have linearly bounded height. The finite Dynkin estimate gives a polynomial box radius, which is absorbed by increasing the exponential scale by a fixed factor.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_compact_cover_word_box_bound line 37
  2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_compact_cover_list_box_bound line 114