OAI/Geometry/IsometricImmersion/Volterra/VolterraDifferentiation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.ODE.intervalExtensionEvalCLM line 11
  2. theorem OAI.SmoothLocal.ODE.intervalExtensionEvalCLM_apply line 16
  3. theorem OAI.SmoothLocal.ODE.intervalExtension_mul line 20
  4. theorem OAI.SmoothLocal.ODE.intervalExtension_family_continuousOn line 25
  5. theorem OAI.SmoothLocal.ODE.intervalExtension_family_hasDerivAt line 35
  6. theorem OAI.SmoothLocal.ODE.intervalExtension_primitive_hasDerivAt line 42
  7. def OAI.SmoothLocal.ODE.volterraScalar line 51
  8. def OAI.SmoothLocal.ODE.volterraVelocity line 54
  9. theorem OAI.SmoothLocal.ODE.volterraScalar_hasDerivAt line 57
  10. theorem OAI.SmoothLocal.ODE.volterraVelocity_hasDerivAt line 77
  11. theorem OAI.SmoothLocal.ODE.volterraScalar_initial line 86
  12. theorem OAI.SmoothLocal.ODE.volterraVelocity_initial line 96
  13. theorem OAI.SmoothLocal.ODE.prescribedVolterraScalar_continuousOn line 100