OAI/Geometry/NearbyLagrangian/CotangentForms.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Cotangent bundle coordinates, Liouville forms and generating maps.

  1. abbrev OAI.NearbyLagrangian.CotangentGeometry.Cotangent line 20
  2. abbrev OAI.NearbyLagrangian.CotangentGeometry.cotangentModel line 23
  3. def OAI.NearbyLagrangian.CotangentGeometry.differentialMap line 28
  4. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiffAt_differentialMap line 31
  5. def OAI.NearbyLagrangian.CotangentGeometry.projection line 47
  6. def OAI.NearbyLagrangian.CotangentGeometry.liouville line 49
  7. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_projection line 53
  8. lemma OAI.NearbyLagrangian.CotangentGeometry.liouville_apply_mfderiv line 59
  9. lemma OAI.NearbyLagrangian.CotangentGeometry.liouville_apply_differentialMap line 67
  10. lemma OAI.NearbyLagrangian.CotangentGeometry.extChartAt_snd line 78
  11. lemma OAI.NearbyLagrangian.CotangentGeometry.extChartAt_fst line 92
  12. lemma OAI.NearbyLagrangian.CotangentGeometry.projection_extChartAt_symm line 98
  13. def OAI.NearbyLagrangian.CotangentGeometry.liouvilleInChart line 112
  14. lemma OAI.NearbyLagrangian.CotangentGeometry.covector_extChartAt_symm line 118
  15. lemma OAI.NearbyLagrangian.CotangentGeometry.mdifferentiableAt_extChartAt_symm line 141
  16. lemma OAI.NearbyLagrangian.CotangentGeometry.mfderiv_projection_extChartAt_symm line 149
  17. theorem OAI.NearbyLagrangian.CotangentGeometry.liouvilleInChart_eq line 175
  18. def OAI.NearbyLagrangian.CotangentGeometry.coordinateLiouville line 189
  19. def OAI.NearbyLagrangian.CotangentGeometry.symplecticForm line 194
  20. theorem OAI.NearbyLagrangian.CotangentGeometry.symplecticForm_eq line 201
  21. def OAI.NearbyLagrangian.CotangentGeometry.generatingMap line 214
  22. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiffAt_generatingMap line 218
  23. theorem OAI.NearbyLagrangian.CotangentGeometry.generatingMap_primitive line 227