OAI/Geometry/NearbyLagrangian/FlatCotangent.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Flat and open cotangent coordinates with Riesz identifications.

  1. def OAI.NearbyLagrangian.CotangentGeometry.cotangentFlatMap line 20
  2. def OAI.NearbyLagrangian.CotangentGeometry.cotangentFlatInv line 22
  3. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentFlat_inCoordinates line 25
  4. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentFlatInv line 33
  5. lemma OAI.NearbyLagrangian.CotangentGeometry.extChartAt_flat line 43
  6. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentFlatMap line 49
  7. def OAI.NearbyLagrangian.CotangentGeometry.cotangentFlatDiffeomorph line 58
  8. lemma OAI.NearbyLagrangian.CotangentGeometry.mfderiv_cotangentFlatMap line 78
  9. lemma OAI.NearbyLagrangian.CotangentGeometry.mfderiv_cotangentFlatInv line 86
  10. theorem OAI.NearbyLagrangian.CotangentGeometry.cotangentFlatInv_symplectic line 97
  11. lemma OAI.NearbyLagrangian.CotangentGeometry.extChartAt_openVal line 113
  12. lemma OAI.NearbyLagrangian.CotangentGeometry.mfderiv_openVal line 116
  13. lemma OAI.NearbyLagrangian.CotangentGeometry.openVal_chart_source line 124
  14. lemma OAI.NearbyLagrangian.CotangentGeometry.openTangent_continuousLinearMapAt line 128
  15. lemma OAI.NearbyLagrangian.CotangentGeometry.openTangent_symmL line 135
  16. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentOpen_inCoordinates line 144
  17. def OAI.NearbyLagrangian.CotangentGeometry.cotangentOpenFlatMap line 156
  18. def OAI.NearbyLagrangian.CotangentGeometry.cotangentOpenFlatInv line 158
  19. lemma OAI.NearbyLagrangian.CotangentGeometry.extChartAt_openFlat line 161
  20. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentOpenFlatInv line 167
  21. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiff_cotangentOpenFlatMap line 177
  22. def OAI.NearbyLagrangian.CotangentGeometry.cotangentOpenFlatDiffeomorph line 196
  23. def OAI.NearbyLagrangian.CotangentGeometry.openPhase line 213
  24. def OAI.NearbyLagrangian.CotangentGeometry.openPhaseDiffeomorph line 216
  25. def OAI.NearbyLagrangian.CotangentGeometry.cotangentOpenRieszDiffeomorph line 237
  26. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentOpenRieszDiffeomorph_apply line 249
  27. def OAI.NearbyLagrangian.CotangentGeometry.phaseRiesz line 264
  28. lemma OAI.NearbyLagrangian.CotangentGeometry.mfderiv_cotangentOpenRiesz line 267
  29. lemma OAI.NearbyLagrangian.CotangentGeometry.cotangentOpenRiesz_symplectic line 286