OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveCoordinateData.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed active-chart coordinate data represent the genuine inverse and amplitude, while vanishing cutoff terms eliminate the other charts.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCoordinateData line 26
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCoordinateData_operator line 40
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.coefficientFrame_inverse line 62
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.primitiveCoordinateData_amplitude line 76