OAI/Geometry/SurfaceImmersion/Correction/FiniteAtlasFreeMetric.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact global free-mode identities for an arbitrary finite family in each fixed atlas chart. This accommodates the variable number of grid cells.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.finiteGlobalPhase line 38
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.finiteGlobalAmplitude line 41
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.finiteAtlasFreeOscillation line 47
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.finiteAtlasFreeOscillation_smooth line 55
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.finite_atlas_zeroPhase line 69
  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.finite_atlas_free_metric line 113