OAI/Geometry/SurfaceImmersion/Correction/GlobalOscillatoryModes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Global phase/amplitude representatives of the actual supported oscillations.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.realMode_smul line 15
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.realMode_zero line 21
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.realMode_contDiff line 25
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surfaceMode line 37
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surfaceMode_tsupport line 40
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.surfaceMode_smooth line 53
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restore_displacement line 63
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorChartRead_mode_on_support line 79
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorChartRead_mode_jets line 88