OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveCoefficientCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

First-derivative bounds for coefficient functionals in each overlapping primitive chart, fixed before choosing any independent phases or radii.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coefficientFrameRead line 32
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coefficientFrame_smoothAt line 37
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coefficientFrameRead_smoothAt line 57
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coefficientFrameRead_C1_bound line 73