OAI/GroupTheory/PolycyclicRecognition/Algebra/LogarithmicCocycleWords.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Sublinear bounds for bounded root words

A finite family of root-coordinate logarithmic estimates is uniform on bounded words with polynomial-exponential amplitude bounds.

  1. theorem OAI.PolycyclicRecognition.sublinear_log_along_smul line 19
  2. theorem OAI.PolycyclicRecognition.IsUnitaryCocycle.norm_word_le line 38
  3. theorem OAI.PolycyclicRecognition.IsUnitaryCocycle.sublinear_bounded_log_words line 45