OAI/Geometry/SurfaceImmersion/Primitive/PrimitiveNormalCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The normal triple estimates imply the actual good phase and injective differential in the plane coordinates used by the exact correction.

  1. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.primitiveNormalTriple_toEuclidean line 14
  2. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.primitiveNormalTriple_chart line 37
  3. theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.good_phase_of_primitive_normal line 52