GenericCurvePhases.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Generic linear parts of the convex quadratic phases have only nondegenerate critical points on each prescribed regular boundary arc.

lemma OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseVelocity_swap line 14
lemma OAI.ClosedSurfaceR4.PhaseGeometry.curvePhaseAcceleration_swap line 20
theorem OAI.ClosedSurfaceR4.PhaseGeometry.curve_phase_all_degenerate_parameters_null line 26

theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_nondegenerate_curve_phases line 63

Source documentation

Countably many regular arcs can be handled in every prescribed open set of phase parameters.

theorem exists_nondegenerate_curve_phases {α : Type*} [Countable α]
    (u v w : α → ℝ → CurvePlane) (hu : ∀ a, ContDiff ℝ ∞ (u a))
    (hv : ∀ a, ContDiff ℝ ∞ (v a))
    (hdu : ∀ a t, HasDerivAt (u a) (v a t) t)
    (hdv : ∀ a t, HasDerivAt (v a) (w a t) t) (L : α → ℝ)
    (U : Set CurvePlane) (hU : IsOpen U) (hne : U.Nonempty) :
    ∃ ell ∈ U, ∀ a t, v a t ≠ 0 → curvePhaseVelocity (u a) (v a) (L a) t ell = 0 →
      curvePhaseAcceleration (u a) (v a) (w a) (L a) t ell ≠ 0 := by
…

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