OAI/Geometry/NearbyLagrangian/CylinderTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Symplectic cylinder charts and transport of their central images.

  1. theorem OAI.NearbyLagrangian.RadialExtension.exists_cylinderEvolution line 23
  2. def OAI.NearbyLagrangian.RadialExtension.IsSymplecticCylinderChart line 48
  3. theorem OAI.NearbyLagrangian.RadialExtension.supported_motion_radial line 58
  4. theorem OAI.NearbyLagrangian.RadialExtension.supported_motion_central line 93
  5. theorem OAI.NearbyLagrangian.Transport.central_open_cylinder_image line 125
  6. theorem OAI.NearbyLagrangian.Transport.central_open_cylinder_image_chart line 146
  7. theorem OAI.NearbyLagrangian.RadialExtension.supported_motion_cylinder_image line 172