CartanGeneratorSchemes.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local generator schemes for the actual Cartan nilpotent factor

The published faithful realization and finite Dynkin formula instantiate the proved local generator scheme with the actual homogeneous Cartan generators.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_local_cartan_generator_scheme line 32
Source documentation
A concrete scheme in the homogeneous generator exponentials covers a nonzero logarithmic neighborhood in the constructed nilpotent factor.
```
theorem exists_local_cartan_generator_scheme
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.CartanWordModel.exists_bounded_cartan_generator_words line 67
Source documentation
A bounded logarithmic set in the actual Cartan factor has a common finite bound on generator word length and on all amplitudes.
```
theorem exists_bounded_cartan_generator_words
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput