OAI/GroupTheory/PolycyclicRecognition/Analysis/InvariantIntegralCurve.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.mulInvariantVectorField_mul line 18
2. theorem OAI.PolycyclicRecognition.IsMIntegralCurveOn.mul_left_invariant line 49
3. theorem OAI.PolycyclicRecognition.exists_global_invariant_integralCurve line 67

   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
   …