OAI/Geometry/SurfaceImmersion/Primitive/PhaseProfileStability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Stability of the five derivative profiles after a fixed nonlinear change of coordinates, with a constant independent of the fast scale.

  1. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.primitiveJetProfile_bound_on line 14
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_profile_correction_bound line 68