ConstructExponential.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Construction of the intrinsic Lie exponential from global integral curves

theorem OAI.PolycyclicRecognition.invariant_integralCurve_unique line 17
theorem OAI.PolycyclicRecognition.invariant_integralCurve_mul_left line 28
def OAI.PolycyclicRecognition.invariantCurve line 37
Source documentation
The global integral curve starting at the identity. Its independence of the existence theorem's choice follows from ODE uniqueness.
```
def invariantCurve (v : GroupLieAlgebra (𝓘(ℝ, E)) G) : ℝ → G :=
…
```
theorem OAI.PolycyclicRecognition.invariantCurve_zero line 40
theorem OAI.PolycyclicRecognition.invariantCurve_isMIntegralCurve line 44
theorem OAI.PolycyclicRecognition.invariantCurve_smul line 48
theorem OAI.PolycyclicRecognition.invariantCurve_add line 55
def OAI.PolycyclicRecognition.groupExponential line 64
Source documentation
The intrinsic exponential, constructed without a Lie-theoretic existence input.
```
def groupExponential (v : GroupLieAlgebra (𝓘(ℝ, E)) G) : G := invariantCurve v 1
```
Mentions: OAI.PolycyclicRecognition.invariantCurve
theorem OAI.PolycyclicRecognition.groupExponential_smul line 66
theorem OAI.PolycyclicRecognition.groupExponential_isGroupExponential line 73
Source documentation
Existence of the Lie exponential with its one-parameter subgroup law and its specified tangent vector at zero.
```
theorem groupExponential_isGroupExponential :
    IsGroupExponential (groupExponential (E := E) (G := G)) where
…
```
Mentions: OAI.PolycyclicRecognition.groupExponential
theorem OAI.PolycyclicRecognition.exists_groupExponential line 100