OAI/GroupTheory/PolycyclicRecognition/Geometry/DominantEigenlineContraction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Contraction toward a dominant real eigenline

A strict spectral gap contracts cones uniformly. The statement is expressed on vectors, so it can later be applied to the projective action without a choice of normalized representatives.

  1. def OAI.PolycyclicRecognition.eigenlineRemainder line 19
  2. theorem OAI.PolycyclicRecognition.eigenlineRemainder_in_ker line 21
  3. theorem OAI.PolycyclicRecognition.eigenlineRemainder_action line 25
  4. theorem OAI.PolycyclicRecognition.eigenline_functional_power line 32
  5. theorem OAI.PolycyclicRecognition.eigenlineRemainder_power_bound line 43
  6. theorem OAI.PolycyclicRecognition.dominant_eigenline_contracts_cones line 61
  7. theorem OAI.PolycyclicRecognition.compact_eigenline_ratio_bound line 92
  8. theorem OAI.PolycyclicRecognition.dominant_eigenline_compact_contraction line 105