OAI/GroupTheory/PolycyclicRecognition/Algebra/EigenlineConeEstimates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Transversality bounds for eigenline cones

Closeness to one line bounds both the norm and evaluation by any functional which does not vanish on that line. These bounds supply the uniform input cones for the dominant-eigenline contraction theorem.

  1. theorem OAI.PolycyclicRecognition.eigenline_cone_norm_bound line 18
  2. theorem OAI.PolycyclicRecognition.eigenline_cone_functional_lower line 31
  3. theorem OAI.PolycyclicRecognition.eigenline_cone_transverse_bound line 47