OAI/Geometry/SurfaceImmersion/Atlas/GoodPhaseC2Stability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The good-phase stability radius uses only the ordinary C2 difference.

  1. lemma OAI.ClosedSurfaceR4.RealModes.coordDeriv_sub_smooth line 12
  2. lemma OAI.ClosedSurfaceR4.RealModes.realTwoJet_sub line 19
  3. lemma OAI.ClosedSurfaceR4.RealModes.norm_realTwoJet_le line 32
  4. theorem OAI.ClosedSurfaceR4.RealModes.compact_good_phase_C2_stability line 53