OAI/Geometry/SurfaceImmersion/Primitive/SurfaceVelocityIdentities.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The leading metric and support of the actual second-jet family.

  1. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.first_slot line 15
  2. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.euclidean_first_derivative line 25
  3. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.leading_xx line 39
  4. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.leading_xy line 51
  5. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.geometry_velocity line 62
  6. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.geometry_mean line 69
  7. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.geometry_dx line 74
  8. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.geometry_dy line 84
  9. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.geometry_initial_zero line 88