OAI/Geometry/IsometricImmersion/Flows/Existence.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.ODE.curvatureField line 15
2. theorem OAI.SmoothLocal.ODE.curvatureField_lipschitz line 18
3. theorem OAI.SmoothLocal.ODE.curvatureField_norm_le line 33
4. theorem OAI.SmoothLocal.ODE.exists_curvature_state_on_closed_interval line 52
5. theorem OAI.SmoothLocal.ODE.curvature_integral_bound line 75
6. theorem OAI.SmoothLocal.ODE.positive_of_integral_bounds line 88