OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothAutonomousCurve.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smoothness bootstrapping for autonomous integral curves

Only the differential equation and smoothness of its vector field are used. This is the local analytic step needed for smooth Lie exponential curves.

  1. theorem OAI.PolycyclicRecognition.contDiffAt_of_autonomous_curve line 20
  2. theorem OAI.PolycyclicRecognition.contDiff_of_autonomous_curve line 37