OAI/GroupTheory/PolycyclicRecognition/Analysis/HarmonicSeparatedRadii.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform separation of the selected word-ball radii

  1. def OAI.PolycyclicRecognition.harmonicRadius line 9
  2. theorem OAI.PolycyclicRecognition.nat_le_sixteen_pow line 11
  3. theorem OAI.PolycyclicRecognition.harmonicRadius_le_two_pow line 19
  4. theorem OAI.PolycyclicRecognition.harmonicRadius_next_ge_eight line 25
  5. theorem OAI.PolycyclicRecognition.harmonicRadius_double_le line 32
  6. theorem OAI.PolycyclicRecognition.exists_harmonic_separation_width line 40
  7. theorem OAI.PolycyclicRecognition.harmonicRadius_quadratic_separation line 50