FlowLocalDifferentiability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual differentiability in initial data for a local autonomous flow. The derivative is obtained from the constructed variational ODE, using the quadratic remainder estimate; it is not an assumed property of the flow.

theorem OAI.PositiveEinsteinFour.FlowCalculus.exists_differentiable_local_flow line 19