OAI/Geometry/SurfaceImmersion/Atlas/AtlasPhaseCatalog.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Fixed finite catalogs for the actual restored global grid phases and their readings in every atlas chart.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.weightedCovectorCatalog line 14
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.mem_weightedCovectorCatalog line 19
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearPhaseCatalog line 34
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restored_linear_phase_mem_catalog line 39
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.linearPhaseCatalog_smooth line 46
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.finiteGlobalPhase_mem_catalog line 55
  7. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localQuadraticPhaseCatalog line 66
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.globalQuadraticPhase_mem_catalog line 71
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.localQuadraticPhaseCatalog_smooth line 89