OAI/Geometry/SurfaceImmersion/Primitive/CircularJetProfiles.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identify the canonical boundary profiles with the actual circular loop in the analytic second-jet coordinates.

  1. lemma OAI.ClosedSurfaceR4.GeometryPreservation.circular_angular_derivative line 15
  2. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.circular_leadingProfileMap line 40