OAI/Geometry/SurfaceImmersion/Atlas/AtlasNormalizationStability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Small C1 perturbations of a spherical immersion remain small after normalization, in the same fixed atlas norm.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.normalized_difference_localization line 21
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.weighted_perturbation_annulus line 44
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.radial_normalization_C1_stability line 55