OAI/Geometry/NearbyLagrangian/PicardPaths.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Smooth Picard paths and global smoothness of complete flows.

  1. lemma OAI.NearbyLagrangian.SmoothFlow.exists_bounded_time_cutoff line 19
  2. lemma OAI.NearbyLagrangian.SmoothFlow.pointwiseLinear_bound line 37
  3. lemma OAI.NearbyLagrangian.SmoothFlow.fderiv_path_equation line 46
  4. lemma OAI.NearbyLagrangian.SmoothFlow.volterra_pointwise_bound line 58
  5. lemma OAI.NearbyLagrangian.SmoothFlow.path_equation_derivative_bound line 65
  6. theorem OAI.NearbyLagrangian.SmoothFlow.smooth_picard_path line 84
  7. lemma OAI.NearbyLagrangian.SmoothFlow.completeFlow_path_equation line 125
  8. theorem OAI.NearbyLagrangian.SmoothFlow.contDiff_capped_flow line 161
  9. theorem OAI.NearbyLagrangian.SmoothFlow.completeFlow_smooth_small_time line 178
  10. theorem OAI.NearbyLagrangian.SmoothFlow.contDiff_completeFlow line 198