OAI/Geometry/NearbyLagrangian/IntrinsicCylinder.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic cylinder charts and generating-family transport.

  1. lemma OAI.NearbyLagrangian.IntrinsicCylinder.baseModel_eq line 31
  2. lemma OAI.NearbyLagrangian.IntrinsicCylinder.cotangentModel_eq line 33
  3. lemma OAI.NearbyLagrangian.IntrinsicCylinder.liouville_eq line 37
  4. lemma OAI.NearbyLagrangian.IntrinsicCylinder.liouvilleInChart_eq line 44
  5. lemma OAI.NearbyLagrangian.IntrinsicCylinder.symplectic_eq line 55
  6. abbrev OAI.NearbyLagrangian.IntrinsicCylinder.Ambient line 65
  7. abbrev OAI.NearbyLagrangian.IntrinsicCylinder.Normal line 66
  8. abbrev OAI.NearbyLagrangian.IntrinsicCylinder.normalPhase line 67
  9. abbrev OAI.NearbyLagrangian.IntrinsicCylinder.ambientPhase line 68
  10. def OAI.NearbyLagrangian.IntrinsicCylinder.sourceCylinderChart line 70
  11. lemma OAI.NearbyLagrangian.IntrinsicCylinder.sourceCylinderChart_apply line 85
  12. def OAI.NearbyLagrangian.IntrinsicCylinder.sourceCylinderDerivative line 90
  13. lemma OAI.NearbyLagrangian.IntrinsicCylinder.sourceCylinderDerivative_eq line 96
  14. theorem OAI.NearbyLagrangian.IntrinsicCylinder.sourceCylinderChart_symplectic line 110
  15. def OAI.NearbyLagrangian.IntrinsicCylinder.centralTube line 139
  16. lemma OAI.NearbyLagrangian.IntrinsicCylinder.centralTube_open line 143
  17. lemma OAI.NearbyLagrangian.IntrinsicCylinder.centralTube_subset line 147
  18. lemma OAI.NearbyLagrangian.IntrinsicCylinder.sourceCylinder_centralImage line 151
  19. lemma OAI.NearbyLagrangian.IntrinsicCylinder.sourceCylinder_zeroImage line 159
  20. def OAI.NearbyLagrangian.IntrinsicCylinder.initialCylinder line 174
  21. theorem OAI.NearbyLagrangian.IntrinsicCylinder.exists_intrinsic_cylinder_transport line 180