OAI/Geometry/SurfaceImmersion/Atlas/GridRestoredGeometry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative normal margins for the restored phases selected on a variable grid in one fixed atlas.

  1. abbrev OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.GridPhaseIndex line 20
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.gridPhaseLabel line 22
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.gridPhaseLabel_injective line 26
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.gridPhaseSupport line 37
  5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.gridRestoredPhase line 40
  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.grid_restored_quadratic_margin line 46