OAI/Geometry/NearbyLagrangian/GeneratingGeometry.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Exactness, isotropy and immersion of generating maps.

  1. def OAI.NearbyLagrangian.Generating.vertical line 16
  2. def OAI.NearbyLagrangian.Generating.momentum line 19
  3. def OAI.NearbyLagrangian.Generating.generatingMap line 22
  4. def OAI.NearbyLagrangian.Generating.localLiouville line 25
  5. def OAI.NearbyLagrangian.Generating.localSymplectic line 27
  6. lemma OAI.NearbyLagrangian.Generating.vertical_hasFDerivAt line 29
  7. lemma OAI.NearbyLagrangian.Generating.momentum_hasFDerivAt line 38
  8. lemma OAI.NearbyLagrangian.Generating.vertical_fderiv_apply line 47
  9. lemma OAI.NearbyLagrangian.Generating.momentum_fderiv_apply line 53
  10. lemma OAI.NearbyLagrangian.Generating.generatingMap_hasFDerivAt line 59
  11. lemma OAI.NearbyLagrangian.Generating.generatingMap_fderiv line 66
  12. theorem OAI.NearbyLagrangian.Generating.liouville_eq_differential line 72
  13. theorem OAI.NearbyLagrangian.Generating.symplectic_eq_zero line 86
  14. theorem OAI.NearbyLagrangian.Generating.generatingMap_ker_injective line 105
  15. theorem OAI.NearbyLagrangian.Generating.generatingMap_mfderiv_injective line 147
  16. theorem OAI.NearbyLagrangian.Generating.generatingMap_mfderiv_isotropic line 184
  17. theorem OAI.NearbyLagrangian.Generating.isotropic_of_exact_coordinates line 217