OAI/Geometry/SurfaceImmersion/Atlas/AtlasGlobalQuadratic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The global finite phase expansion has the quadratic mean determined by its phase data.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_global_zeroPhase line 36
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlasGlobalNonzero line 82
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_free_global_metric line 92
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.atlas_quadratic_oscillation_eq_global line 114