OAI/Geometry/SurfaceImmersion/Primitive/FrozenCircularData.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The normal data as smooth functions of position and angular value. The first mixed normal coefficient contains no derivative of the angle.

  1. def OAI.ClosedSurfaceR4.VelocityFrame.frozenError line 17
  2. def OAI.ClosedSurfaceR4.VelocityFrame.frozenNormal line 22
  3. def OAI.ClosedSurfaceR4.VelocityFrame.frozenSize line 27
  4. def OAI.ClosedSurfaceR4.VelocityFrame.frozenFirst line 31
  5. lemma OAI.ClosedSurfaceR4.VelocityFrame.frozenError_smoothOn line 34
  6. theorem OAI.ClosedSurfaceR4.VelocityFrame.frozen_normals_smoothOn line 56
  7. theorem OAI.ClosedSurfaceR4.VelocityFrame.frozen_coefficients_smoothOn line 98
  8. theorem OAI.ClosedSurfaceR4.VelocityFrame.actual_first_eq_frozen line 111