OAI/GroupTheory/PolycyclicRecognition/Geometry/ValuedEigenlineContraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Eigenline contraction over a normed coefficient field

The field change in Tits, Section 4, need not give the original real norm. This is the concrete linear estimate needed after such a change; no field embedding or contracting representation is assumed to exist here.

  1. def OAI.PolycyclicRecognition.ValuedLinearDynamics.remainder line 17
  2. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.remainder_in_ker line 19
  3. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.remainder_action line 23
  4. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.functional_power line 29
  5. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.remainder_power_bound line 40
  6. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.contracts_cones line 57