OAI/Geometry/NearbyLagrangian/SymplecticCylinder.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Symplectic radial cylinder charts and central spatial images.

  1. theorem OAI.NearbyLagrangian.diffeomorph_preservesForm_trans line 29
  2. theorem OAI.NearbyLagrangian.diffeomorph_preservesForm_symm line 44
  3. theorem OAI.NearbyLagrangian.diffeomorph_preservesForm_prodRight line 59
  4. def OAI.NearbyLagrangian.CotangentGeometry.radialCotangentDiffeomorph line 96
  5. def OAI.NearbyLagrangian.CotangentGeometry.cotangentCylinderChart line 104
  6. lemma OAI.NearbyLagrangian.CotangentGeometry.radialCotangentDiffeomorph_symplectic line 112
  7. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentLift_openRiesz_symplectic line 132
  8. theorem OAI.NearbyLagrangian.CotangentGeometry.cotangentCylinderChart_symplectic line 145
  9. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentCylinderChart_position line 191
  10. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentCylinderChart_zero line 197
  11. def OAI.NearbyLagrangian.CotangentGeometry.centralSpatial line 231
  12. lemma OAI.NearbyLagrangian.CotangentGeometry.centralSpatial_subset line 236
  13. lemma OAI.NearbyLagrangian.CotangentGeometry.centralSpatial_isOpen line 243
  14. theorem OAI.NearbyLagrangian.CotangentGeometry.cotangentCylinderChart_centralImage line 252
  15. theorem OAI.NearbyLagrangian.CotangentGeometry.cotangentCylinderChart_zeroImage line 277