OAI/GroupTheory/PolycyclicRecognition/Geometry/ChartedExponentialFlow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The right exponential flow in an identity chart

  1. def OAI.PolycyclicRecognition.chartExponentialFlow line 18

    Source documentation

    Right multiplication is the flow of the left-invariant field.

    def chartExponentialFlow (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (v : E)
    (q : ℝ × E) : ℝ × E :=
…
  2. theorem OAI.PolycyclicRecognition.contDiffAt_chartExponentialFlow line 23
  3. theorem OAI.PolycyclicRecognition.chartExponentialFlow_zero line 50
  4. theorem OAI.PolycyclicRecognition.fderiv_chartExponentialFlow_vertical_zero line 60
  5. theorem OAI.PolycyclicRecognition.hasDerivAt_chartExponentialFlow_time line 80
  6. theorem OAI.PolycyclicRecognition.fderiv_chartExponentialFlow_time line 111
  7. theorem OAI.PolycyclicRecognition.fderiv_chartExponentialFlow_field line 125