OAI/Geometry/SurfaceImmersion/Primitive/JetVelocityCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Euclidean coordinates for the geometric velocity and the actual ordered jets used in the finite periodic expansion.

  1. abbrev OAI.ClosedSurfaceR4.JetVelocityCoordinates.Euclidean line 15
  2. def OAI.ClosedSurfaceR4.JetVelocityCoordinates.toEuclidean line 17
  3. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.inner_toEuclidean line 19
  4. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.gram_toEuclidean line 24
  5. def OAI.ClosedSurfaceR4.JetVelocityCoordinates.slot line 29
  6. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.slot_smooth line 31
  7. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.slot_decode_x line 36
  8. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.slot_decode_y line 37
  9. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.slot_decode_yy line 38
  10. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.slot_y_derivative line 40
  11. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.euclidean_y_derivative line 52
  12. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.tangential_part_perp line 64