OAI/Geometry/SurfaceImmersion/Primitive/ActualCircularPeriod.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Representatives in one compact period transfer the constructed surface profile estimates to the analytic loop at every phase.

  1. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.actual_circular_period_profile line 14