OAI/Geometry/NearbyLagrangian/PolarCharts.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Polar and Euclidean cylinder diffeomorphisms.

  1. def OAI.NearbyLagrangian.PolarCylinder.radialWindow line 15
  2. def OAI.NearbyLagrangian.PolarCylinder.annulus line 16
  3. lemma OAI.NearbyLagrangian.PolarCylinder.radial_pos line 19
  4. lemma OAI.NearbyLagrangian.PolarCylinder.annulus_norm_pos line 24
  5. lemma OAI.NearbyLagrangian.PolarCylinder.annulus_ne_zero line 29
  6. def OAI.NearbyLagrangian.PolarCylinder.polarMap line 32
  7. def OAI.NearbyLagrangian.PolarCylinder.polarInv line 41
  8. lemma OAI.NearbyLagrangian.PolarCylinder.polarInv_polarMap line 54
  9. lemma OAI.NearbyLagrangian.PolarCylinder.polarMap_polarInv line 69
  10. lemma OAI.NearbyLagrangian.PolarCylinder.contMDiff_polarMap line 77
  11. lemma OAI.NearbyLagrangian.PolarCylinder.contMDiff_polarInv line 84
  12. def OAI.NearbyLagrangian.PolarCylinder.polarDiffeomorph line 100
  13. def OAI.NearbyLagrangian.PolarCylinder.productPolarDiffeomorph line 119
  14. def OAI.NearbyLagrangian.PolarCylinder.productOpen line 153
  15. def OAI.NearbyLagrangian.PolarCylinder.productOpenDiffeomorph line 156
  16. def OAI.NearbyLagrangian.PolarCylinder.linearOpen line 175
  17. def OAI.NearbyLagrangian.PolarCylinder.linearOpenDiffeomorph line 178
  18. def OAI.NearbyLagrangian.PolarCylinder.euclideanCylinderOpen line 194
  19. def OAI.NearbyLagrangian.PolarCylinder.euclideanCylinderDiffeomorph line 200
  20. def OAI.NearbyLagrangian.generalProductDiffeomorph line 229
  21. def OAI.NearbyLagrangian.PolarCylinder.radialCoordinates line 241
  22. def OAI.NearbyLagrangian.PolarCylinder.radialSquare line 245
  23. def OAI.NearbyLagrangian.PolarCylinder.radialSquareDiffeomorph line 248
  24. def OAI.NearbyLagrangian.PolarCylinder.euclideanCylinderSquareDiffeomorph line 254
  25. def OAI.NearbyLagrangian.PolarCylinder.flatEuclideanCylinderSquareDiffeomorph line 272
  26. lemma OAI.NearbyLagrangian.PolarCylinder.mem_radialSquare_iff line 282