OAI/Geometry/SurfaceImmersion/Primitive/UniformScaledLongitudinalProfile.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform control of the rescaled longitudinal second derivative of the actual finite primitive.

  1. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.slot_x_derivative line 16
  2. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.euclidean_x_derivative line 27
  3. lemma OAI.ClosedSurfaceR4.JetVelocityCoordinates.norm_slot_le line 39
  4. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.uniform_scaled_longitudinal_profile line 50