OAI/Geometry/SurfaceImmersion/Primitive/JetVelocityLoop.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A controlled loop on a neighborhood of the actual second-jet section. Its translation depends on position alone, so the prescribed turn derivatives along the original section persist under the joint density construction.

  1. abbrev OAI.ClosedSurfaceR4.CollarVelocity.JetBase line 17
  2. def OAI.ClosedSurfaceR4.CollarVelocity.jetSection line 19
  3. lemma OAI.ClosedSurfaceR4.CollarVelocity.jetSection_smooth line 21
  4. def OAI.ClosedSurfaceR4.CollarVelocity.jetAngle line 24
  5. lemma OAI.ClosedSurfaceR4.CollarVelocity.jetAngle_on_section line 28
  6. theorem OAI.ClosedSurfaceR4.CollarVelocity.controlled_jet_loop line 34