OAI/GroupTheory/PolycyclicRecognition/Algebra/ConstructedNilpotentInputs.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Constructed nilpotent models with their BCH and Haar data

Polynomial exponential coordinates give nilpotent Lie models together with their finite BCH expansion and exponential Haar measure.

  1. theorem OAI.PolycyclicRecognition.polynomialCoordinateLieModel_dynkin line 19
  2. theorem OAI.PolycyclicRecognition.polynomialCoordinateLieModel_haar line 25
  3. theorem OAI.PolycyclicRecognition.exists_nilpotent_model_with_inputs line 32
  4. theorem OAI.PolycyclicRecognition.exists_nilpotent_model_with_inputs_of_finite line 40