OAI/GroupTheory/PolycyclicRecognition/Geometry/DynkinLocalExponential.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local regularity of the intrinsic exponential from BCH

The BCH basis-input polynomial has identity derivative. Composing its local inverse with the smooth product of one-parameter subgroups constructs local exponential coordinates, without an assumed global logarithm.

  1. theorem OAI.PolycyclicRecognition.exponentialProduct_eq_list_prod line 25
  2. theorem OAI.PolycyclicRecognition.exponential_comp_basisDynkinParameter line 36
  3. theorem OAI.PolycyclicRecognition.local_exponential_regularity_of_dynkin line 50