OAI/Geometry/SurfaceImmersion/Primitive/CircularBoundaryParam.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Explicit regular parametrizations of the actual coordinate circles. The compact parameter interval covers the whole boundary.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.circularParam line 15
  2. def OAI.ClosedSurfaceR4.PhaseGeometry.circularVelocity line 18
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularParam_smooth line 20
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularParam_hasDerivAt line 24
  5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularVelocity_ne_zero line 33
  6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularParam_radius line 40
  7. lemma OAI.ClosedSurfaceR4.PhaseGeometry.circularParam_covers line 45
  8. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularBoundary line 70
  9. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularBoundaryParam line 74
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularBoundaryParam_target line 78
  11. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularBoundaryParam_smooth line 83
  12. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularBoundary_image line 92
  13. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularBoundary_compact line 106