OAI/Geometry/SurfaceImmersion/Primitive/ActualCircularProfile.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed real surface profile is exactly the analytic loop's five-profile map, including its transverse mixed derivative.

  1. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.actual_circular_geometric_profile line 16