OAI/GroupTheory/PolycyclicRecognition/Analysis/HarmonicGoodScales.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Two separated scales with controlled growth

The multiplicative form of Kleiner's good-scale argument, Section 3.1.

  1. theorem OAI.PolycyclicRecognition.exists_adjacent_ratio_of_block_bound line 11
  2. theorem OAI.PolycyclicRecognition.two_good_scales_of_block_bound line 30
  3. theorem OAI.PolycyclicRecognition.exponential_growth_two_good_scales line 53