OAI/Geometry/SurfaceImmersion/Atlas/PhaseCovectorFamily.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compact parameter bounds for the actual circular phase differentials, including their first spatial derivatives.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseCovectorRead line 19
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseCovectorRead_smoothOn line 24
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularCovectorJoint line 30
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularCovectorJoint_smoothOn line 36
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularCovectorJoint_eq line 56
  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circular_covector_parameter_bound line 87