OAI/GroupTheory/PolycyclicRecognition/Algebra/OneSidedDominantDynamics.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

One-sided spectral gaps contradict polynomial growth

Two transverse attracting eigenlines give disjoint forward invariant cones for suitable positive powers. Counting positive words needs no inverse gap.

  1. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.forward_cones_of_dominant_eigenlines line 19
  2. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.polynomial_growth_excludes_transverse_dominant_eigenlines line 71
  3. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.polynomial_growth_excludes_asymptotically_dominant_eigenlines line 117