LieIntegrationNaturality.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Removing exponential compatibility from the integration input

Only existence of a smooth homomorphism with the prescribed differential remains from Lee's integration theorem. The exponential maps and their compatibility are supplied by the proved integral-curve construction.

def OAI.PolycyclicRecognition.NilpotentSmoothIntegrationInput line 26
Source documentation
The still-undischarged existence assertion of Lee (2013), Theorem 20.19, in precisely the nilpotent-source specialization used in the application.
```
def NilpotentSmoothIntegrationInput : Prop :=
…
```
theorem OAI.PolycyclicRecognition.nilpotentLieIntegrationInput_of_smooth line 32
theorem OAI.PolycyclicRecognition.nilpotentLieIntegrationInput_iff_smooth line 44
Source documentation
Smooth integration is equivalent to integration compatible with the intrinsic exponential maps.
```
theorem nilpotentLieIntegrationInput_iff_smooth [T2Space N] [T2Space G] :
    NilpotentLieIntegrationInput (EN := EN) (N := N) (EG := EG) (G := G) ↔
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentLieIntegrationInput