SmoothLieExponential.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The intrinsic exponential for the smooth rotational graph

The same invariant-field ODE construction works at C-infinity regularity. This concrete version avoids imposing an analytic atlas on the new graph.

theorem OAI.PolycyclicRecognition.SmoothLie.mulInvariantVectorField_mul line 25
theorem OAI.PolycyclicRecognition.SmoothLie.IsMIntegralCurveOn.mul_left_invariant line 56
theorem OAI.PolycyclicRecognition.SmoothLie.exists_global_invariant_integralCurve line 74
Source documentation
A fixed local existence time at the identity works at every point by left translation, so the manifold uniform-time theorem supplies global curves.
```
theorem exists_global_invariant_integralCurve [T2Space G]
    (v : GroupLieAlgebra (𝓘(ℝ, E)) G) (x : G) :
    ∃ γ : ℝ → G, γ 0 = x ∧ IsMIntegralCurve (I := 𝓘(ℝ, E)) γ (mulInvariantVectorField v) := by
…
```
theorem OAI.PolycyclicRecognition.SmoothLie.invariant_integralCurve_unique line 95
theorem OAI.PolycyclicRecognition.SmoothLie.invariant_integralCurve_mul_left line 106
def OAI.PolycyclicRecognition.SmoothLie.invariantCurve line 115
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.SmoothLie.invariantCurve_zero line 118
theorem OAI.PolycyclicRecognition.SmoothLie.invariantCurve_isMIntegralCurve line 122
theorem OAI.PolycyclicRecognition.SmoothLie.invariantCurve_smul line 126
theorem OAI.PolycyclicRecognition.SmoothLie.invariantCurve_add line 133
def OAI.PolycyclicRecognition.SmoothLie.groupExponential line 142
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.SmoothLie.invariantCurve
theorem OAI.PolycyclicRecognition.SmoothLie.groupExponential_smul line 144
theorem OAI.PolycyclicRecognition.SmoothLie.groupExponential_isGroupExponential line 151
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.SmoothLie.groupExponential
theorem OAI.PolycyclicRecognition.SmoothLie.exists_groupExponential line 178