OAI/GroupTheory/PolycyclicRecognition/Geometry/ContractedNilpotentFlow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Contracting flows give explicit contracted elements

Polynomial factors from a nilpotent Jordan correction decay under a negative real weight. This produces the actual sequence required by contractedBy.

  1. theorem OAI.PolycyclicRecognition.tendsto_contracted_nilpotent_flow line 19
  2. theorem OAI.PolycyclicRecognition.contractedBy_of_continuous_flow line 39