OAI/Geometry/SurfaceImmersion/Atlas/CurvePhaseParameterGraph.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A chart of the critical-point equation for an affine perturbation of a quadratic phase along a regular plane curve.

  1. abbrev OAI.ClosedSurfaceR4.PhaseGeometry.CurvePlane line 12
  2. def OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseVelocity line 14
  3. def OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseAcceleration line 17
  4. def OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseParameterGraph line 21
  5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseParameterGraph_eq line 25
  6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseParameterGraph_deriv_zero line 35