OAI/Geometry/SurfaceImmersion/Atlas/CenteredParabolicChart.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

One explicit nonlinear phase chart on a whole centered neighborhood.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.phaseCovectorSquare line 13
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phaseCovectorSquare_pos line 15
  3. def OAI.ClosedSurfaceR4.PhaseGeometry.centeredPhaseCoordinates line 18
  4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredPhaseCoordinates_apply line 21
  5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredPhaseCoordinates_smooth line 25
  6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredPhaseCoordinates_inverse_smooth line 29
  7. def OAI.ClosedSurfaceR4.PhaseGeometry.centeredParabolicChart line 34
  8. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredParabolicChart_phase line 40
  9. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredParabolicChart_smooth line 51
  10. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredParabolicChart_inverse_smooth line 55
  11. lemma OAI.ClosedSurfaceR4.PhaseGeometry.centeredParabolicChart_source line 62