OAI/Geometry/NearbyLagrangian/SmoothFamilies.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Smooth homogeneous families and regular critical parametrizations.

  1. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.SmoothFamily line 20
  2. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiffAt_family_fderiv line 26
  3. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiffAt_family_gradient line 39
  4. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiff_family_gradient line 49
  5. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiff_family_direction line 62
  6. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiff_family_radialSolution line 77
  7. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.mfderiv_family_radialSolution_injective line 94
  8. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.SmoothFamily.smoothOffZero line 149
  9. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.familyCriticalParam line 156
  10. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiff_familyCriticalParam line 161
  11. abbrev OAI.NearbyLagrangian.Tubes.RegularHomogeneous.FamilyCriticalLocus line 169
  12. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.familyCriticalHomeomorph line 173
  13. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.mfderiv_familyCriticalParam_injective line 209
  14. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contDiffAt_gradient line 238
  15. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.gradient_radial_derivative line 245
  16. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contDiffAt_gradient_direction line 261
  17. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contDiffAt_radial_solution line 268
  18. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiff_direction line 274
  19. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiff_radialSolution line 284
  20. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.contMDiff_criticalParametrization line 292
  21. def OAI.NearbyLagrangian.Tubes.RegularHomogeneous.criticalEquation line 299
  22. lemma OAI.NearbyLagrangian.Tubes.RegularHomogeneous.criticalEquation_mfderiv line 303
  23. theorem OAI.NearbyLagrangian.Tubes.RegularHomogeneous.criticalEquation_regular line 318