OAI/Geometry/SurfaceImmersion/Atlas/AtlasNormalizationBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A fixed C2 atlas budget for radial normalization. A smooth extension through zero is used only outside the region contributing to localization.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.normalized_localization_eq line 20
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.radial_normalization_smooth line 36
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.chartWeight_square_compact line 45
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.exists_weighted_bound line 55
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.radial_normalization_C2_budget line 65