OAI/GroupTheory/PolycyclicRecognition/Analysis/LocalProfileAffinity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local profile affinity from the actual finite flow labels

The proof uses admissible generator words and the inverse function theorem; it does not assume a smooth profile or a hypoellipticity conclusion.

  1. theorem OAI.PolycyclicRecognition.affine_of_small_generator_increments line 30
  2. theorem OAI.PolycyclicRecognition.affine_on_flow_neighborhood line 63