OAI/Geometry/NearbyLagrangian/CylinderRegularity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Regularity, injectivity and restoration for intrinsic cylinder families.

  1. lemma OAI.NearbyLagrangian.CotangentGeometry.contMDiffAt_intrinsicVertical line 29
  2. theorem OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily_regular line 43
  3. lemma OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily_vertical_joint line 104
  4. def OAI.NearbyLagrangian.CotangentGeometry.cylinderCriticalPhaseEquiv line 115
  5. lemma OAI.NearbyLagrangian.CotangentGeometry.phaseGenerate_cylinderFamily line 130
  6. theorem OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily_morseOn line 145
  7. theorem OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily_phase_range line 168
  8. theorem OAI.NearbyLagrangian.CotangentGeometry.cylinderFamily_phase_injective line 188
  9. theorem OAI.NearbyLagrangian.IntrinsicCylinder.exists_intrinsic_restored_endpoint line 226