OAI/Geometry/SurfaceImmersion/Primitive/VelocityCoordinateData.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Smooth velocity coordinates and their calibrated collar values.

  1. lemma OAI.ClosedSurfaceR4.VelocityFrame.dot_smoothOn line 15
  2. lemma OAI.ClosedSurfaceR4.VelocityFrame.plane_coordinates_smoothOn line 20
  3. lemma OAI.ClosedSurfaceR4.VelocityFrame.norm_smul_normalize line 30
  4. lemma OAI.ClosedSurfaceR4.VelocityFrame.dot_normalize_self line 34
  5. lemma OAI.ClosedSurfaceR4.VelocityFrame.collar_coordinates line 42
  6. def OAI.ClosedSurfaceR4.VelocityFrame.velocityRadius line 52
  7. lemma OAI.ClosedSurfaceR4.VelocityFrame.velocityRadius_sq line 54
  8. lemma OAI.ClosedSurfaceR4.VelocityFrame.velocityRadius_pos line 59
  9. lemma OAI.ClosedSurfaceR4.VelocityFrame.velocityRadius_smoothOn line 67