OAI/Geometry/NearbyLagrangian/RealizationRegularity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Critical annuli, regular vertical equations and isotropic realization.

  1. lemma OAI.NearbyLagrangian.EmbeddedRealization.sourceFamily_eq_uncut line 25
  2. lemma OAI.NearbyLagrangian.EmbeddedRealization.fderiv_sourceFamily_of_annulus line 34
  3. lemma OAI.NearbyLagrangian.EmbeddedRealization.sourceFamily_eq_neg_at_critical line 55
  4. lemma OAI.NearbyLagrangian.EmbeddedRealization.critical_annulus line 69
  5. def OAI.NearbyLagrangian.EmbeddedRealization.sourceVertical line 88
  6. theorem OAI.NearbyLagrangian.EmbeddedRealization.sourceVertical_fixed_regular line 94
  7. lemma OAI.NearbyLagrangian.EmbeddedRealization.contMDiff_sourceVertical line 144
  8. theorem OAI.NearbyLagrangian.EmbeddedRealization.sourceVertical_regular line 153
  9. theorem OAI.NearbyLagrangian.EmbeddedRealization.sourceGeneratingMap_isotropic line 197
  10. theorem OAI.NearbyLagrangian.EmbeddedRealization.sourceGeneratingMap_mfderiv_injective line 228