OAI/Geometry/SurfaceImmersion/Primitive/ControlledInteriorLoop.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Assemble the interior velocity angle: a small translation with large turn jets, an actual positive density, the exact prescribed vector mean, and exactly two turns. No density or transverse-correction solvability is assumed.

  1. def OAI.ClosedSurfaceR4.CollarVelocity.normalizedAngle line 16
  2. lemma OAI.ClosedSurfaceR4.CollarVelocity.unitAngle_periodic line 20
  3. theorem OAI.ClosedSurfaceR4.CollarVelocity.controlled_interior_loop line 24