OAI/Geometry/NearbyLagrangian/CotangentModel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Cotangent forms, exact Lagrangian embeddings and Hamiltonian isotopies.

  1. abbrev OAI.NearbyLagrangian.Sphere line 13
  2. abbrev OAI.NearbyLagrangian.Base line 14
  3. abbrev OAI.NearbyLagrangian.BaseVector line 15
  4. abbrev OAI.NearbyLagrangian.baseModel line 16
  5. abbrev OAI.NearbyLagrangian.Cotangent line 17
  6. abbrev OAI.NearbyLagrangian.CotangentVector line 20
  7. abbrev OAI.NearbyLagrangian.cotangentModel line 21
  8. def OAI.NearbyLagrangian.projection line 24
  9. def OAI.NearbyLagrangian.zeroSection line 26
  10. def OAI.NearbyLagrangian.liouville line 28
  11. def OAI.NearbyLagrangian.liouvilleInChart line 32
  12. def OAI.NearbyLagrangian.symplecticForm line 38
  13. def OAI.NearbyLagrangian.IsClosedExactLagrangian line 45
  14. abbrev OAI.NearbyLagrangian.CotangentDiffeomorph line 58
  15. def OAI.NearbyLagrangian.IsCompactHamiltonianIsotopy line 61
  16. def OAI.NearbyLagrangian.IsHamiltonianImage line 75
  17. def OAI.NearbyLagrangian.MainStatement line 80