OAI/Geometry/NearbyLagrangian/CompleteFlow.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Complete bounded Lipschitz flows, support and first integrals.

  1. structure OAI.NearbyLagrangian.ODE.CompleteFlow line 14
  2. theorem OAI.NearbyLagrangian.ODE.exists_local_box_flow line 20
  3. theorem OAI.NearbyLagrangian.ODE.box_flow_agree line 41
  4. theorem OAI.NearbyLagrangian.ODE.exists_completeFlow line 65
  5. theorem OAI.NearbyLagrangian.ODE.CompleteFlow.add line 130
  6. def OAI.NearbyLagrangian.ODE.CompleteFlow.homeomorph line 143
  7. theorem OAI.NearbyLagrangian.ODE.CompleteFlow.fixed line 155
  8. theorem OAI.NearbyLagrangian.ODE.CompleteFlow.displacement_support_subset line 164
  9. theorem OAI.NearbyLagrangian.ODE.CompleteFlow.first_integral line 171
  10. theorem OAI.NearbyLagrangian.ODE.compact_field_bounds line 183
  11. theorem OAI.NearbyLagrangian.ODE.exists_completeFlow_of_compact line 198