OAI/Geometry/NearbyLagrangian/RestoredRestriction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Restriction and restoration of a tame family with one critical point.

  1. def OAI.NearbyLagrangian.Transport.TameOn.referenceAt line 20
  2. lemma OAI.NearbyLagrangian.Transport.TameOn.referenceAt_apply line 33
  3. lemma OAI.NearbyLagrangian.Transport.TameOn.referenceAt_fderiv line 36
  4. lemma OAI.NearbyLagrangian.Transport.TameOn.continuous_referenceAt line 40
  5. def OAI.NearbyLagrangian.Transport.TameOn.restrictedReference line 58
  6. lemma OAI.NearbyLagrangian.Transport.TameOn.restricted_estimates line 63
  7. lemma OAI.NearbyLagrangian.Transport.TameOn.contMDiff_restrict line 90
  8. theorem OAI.NearbyLagrangian.Transport.TameOn.exists_restored_restriction line 110
  9. lemma OAI.NearbyLagrangian.Transport.TameOn.partial_hessian_eq line 149
  10. theorem OAI.NearbyLagrangian.Transport.TameOn.exists_restored_single_critical line 168