OAI/Geometry/NearbyLagrangian/GeneratingEmbeddings.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Generating-map immersions and closed exact Lagrangian embeddings.

  1. def OAI.NearbyLagrangian.CotangentGeometry.vertical line 24
  2. def OAI.NearbyLagrangian.CotangentGeometry.familyInChart line 27
  3. def OAI.NearbyLagrangian.CotangentGeometry.criticalCoordinates line 30
  4. def OAI.NearbyLagrangian.CotangentGeometry.criticalCoordinatesInv line 33
  5. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiffAt_criticalCoordinates line 36
  6. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiffAt_criticalCoordinatesInv line 48
  7. lemma OAI.NearbyLagrangian.CotangentGeometry.contDiffAt_familyInChart line 60
  8. lemma OAI.NearbyLagrangian.CotangentGeometry.vertical_familyInChart line 67
  9. lemma OAI.NearbyLagrangian.CotangentGeometry.vertical_chart_comp_eventually line 75
  10. lemma OAI.NearbyLagrangian.CotangentGeometry.vertical_familyInChart_regular line 86
  11. lemma OAI.NearbyLagrangian.CotangentGeometry.generatingMap_in_chart line 108
  12. theorem OAI.NearbyLagrangian.CotangentGeometry.generatingMap_mfderiv_injective line 142
  13. theorem OAI.NearbyLagrangian.CotangentGeometry.generatingMap_isImmersion line 219
  14. theorem OAI.NearbyLagrangian.CotangentGeometry.generatingMap_isotropic line 253
  15. theorem OAI.NearbyLagrangian.CotangentGeometry.generatingMap_closed_exact_embedding line 292