OAI/Geometry/NearbyLagrangian/CotangentLifts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth cotangent lifts of diffeomorphisms and their symplecticity.

  1. def OAI.NearbyLagrangian.CotangentGeometry.cotangentLiftMap line 25
  2. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiffAt_cotangentLiftMap line 29
  3. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentLiftMap line 71
  4. lemma OAI.NearbyLagrangian.CotangentGeometry.mfderiv_diffeomorph_inverse_comp line 76
  5. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentLiftMap_inverse line 86
  6. def OAI.NearbyLagrangian.CotangentGeometry.cotangentLift line 99
  7. theorem OAI.NearbyLagrangian.CotangentGeometry.cotangentLift_liouville line 109
  8. theorem OAI.NearbyLagrangian.CotangentGeometry.cotangentLift_symplectic line 147