OAI/Geometry/SurfaceImmersion/Primitive/CircularPhaseDependence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact affine dependence of supported circular phases on their linear parameters. The curvature parameter stays fixed.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularPhase line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularPhase_smooth line 23
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularPhase_sub line 29
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.circularPhase_mfderiv_sub line 44