OAI/GroupTheory/PolycyclicRecognition/Analysis/SequenceVolumeComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exponential volume comparison along the profile-scale sequence

  1. theorem OAI.PolycyclicRecognition.subexponential_upper_polynomial line 13
  2. theorem OAI.PolycyclicRecognition.exponent_le_of_sequence_polynomial_bound line 26
  3. theorem OAI.PolycyclicRecognition.exponent_le_of_sequence_separated_counts line 35