OAI/Geometry/SurfaceImmersion/Primitive/UniformPrimitiveProfiles.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

All five actual derivative profiles share a loss fixed before the slow map. The leading profiles are the geometric velocity and its derivatives.

  1. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.primitiveJetProfile line 16
  2. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.uniform_primitive_five_profiles line 27