OAI/GroupTheory/PolycyclicRecognition/Algebra/SequenceSubexponential.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Subexponential estimates along the actual sequence of profile scales

  1. def OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq line 15
  2. def OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq line 18
  3. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBound.along_sequence line 21
  4. theorem OAI.PolycyclicRecognition.HasSubexponentialUpperBound.along_sequence line 26
  5. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq.eventually_pos line 31
  6. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq.mono line 35
  7. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq.mul line 42
  8. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBoundSeq.div line 52
  9. theorem OAI.PolycyclicRecognition.exists_slow_sequence_selection line 63
  10. theorem OAI.PolycyclicRecognition.exists_slow_sequence_subexponential_mass line 79
  11. theorem OAI.PolycyclicRecognition.exponent_le_of_sequence_subexponential_bounds line 100