OAI/Geometry/NearbyLagrangian/NearIdentity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Smooth inverses and mixed maps near the identity.

  1. def OAI.NearbyLagrangian.Transport.nearIdentityHomeomorph line 18
  2. lemma OAI.NearbyLagrangian.Transport.nearIdentityHomeomorph_apply line 36
  3. def OAI.NearbyLagrangian.Transport.nearIdentityDerivative line 41
  4. lemma OAI.NearbyLagrangian.Transport.nearIdentityDerivative_coe line 47
  5. theorem OAI.NearbyLagrangian.Transport.nearIdentityHomeomorph_smooth_inverse line 54
  6. def OAI.NearbyLagrangian.Transport.mixedMap line 73
  7. def OAI.NearbyLagrangian.Transport.spatialBlock line 75
  8. lemma OAI.NearbyLagrangian.Transport.spatialBlock_apply line 77
  9. lemma OAI.NearbyLagrangian.Transport.norm_spatialBlock_le line 79
  10. lemma OAI.NearbyLagrangian.Transport.contDiff_mixedMap line 85
  11. lemma OAI.NearbyLagrangian.Transport.hasFDerivAt_mixedMap line 88
  12. lemma OAI.NearbyLagrangian.Transport.mixedMap_fderiv_sub line 93
  13. lemma OAI.NearbyLagrangian.Transport.mixedMap_small line 100
  14. def OAI.NearbyLagrangian.Transport.mixedHomeomorph line 110
  15. lemma OAI.NearbyLagrangian.Transport.mixedHomeomorph_apply line 117
  16. lemma OAI.NearbyLagrangian.Transport.contDiff_mixedHomeomorph_symm line 122