OAI/Geometry/NearbyLagrangian/ImplicitRoots.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth parameter-dependent roots and near-identity inverses.

  1. theorem OAI.NearbyLagrangian.Transport.contDiff_unique_root line 19
  2. lemma OAI.NearbyLagrangian.Transport.fderiv_slice_right line 34
  3. theorem OAI.NearbyLagrangian.Transport.contDiff_nearIdentity_inverse line 41
  4. theorem OAI.NearbyLagrangian.Transport.exists_contDiff_nearIdentity_inverse line 65