OAI/Geometry/SurfaceImmersion/Atlas/CurvePhaseCriticalValues.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Degenerate tangencies along a curve form a null set of linear phase parameters. The first-coordinate chart of the critical equation suffices where the first velocity component is nonzero.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseParameterGraph_differentiableAt line 15
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseParameterGraph_singular line 33
  3. theorem OAI.ClosedSurfaceR4.PhaseGeometry.curve_phase_degenerate_parameters_null line 55

    Source documentation

    The bad parameter set is contained in the critical values of the explicit two-dimensional parameter graph.

    theorem curve_phase_degenerate_parameters_null
    (u v w : ℝ → CurvePlane) (hu : ContDiff ℝ ∞ u) (hv : ContDiff ℝ ∞ v)
    (hdu : ∀ t, HasDerivAt u (v t) t) (hdv : ∀ t, HasDerivAt v (w t) t) (L : ℝ) :
    volume {ell : CurvePlane | ∃ t, (v t).1 ≠ 0 ∧
      curvePhaseVelocity u v L t ell = 0 ∧ curvePhaseAcceleration u v w L t ell = 0} = 0 := by
…

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.CurvePlane, OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseVelocity, OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseAcceleration