OAI/Geometry/SurfaceImmersion/Atlas/PhaseCoordinateCovector.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The first phase coordinate has the exact covector used by the local rank-one tensor pullback.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.firstPhaseCovector_apply line 16
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.jetChart_tangentCoordinates line 33
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseFirst_mfderiv line 50