OAI/Geometry/SurfaceImmersion/Atlas/UniformMetricPhaseGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

One C2 neighborhood preserves all fixed metric-adapted phase geometry, independently of every smoothing and correction order.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.compact_read_phase_C2_stability line 24
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.phaseDerivative_linear line 65
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.uniform_C2_geometry line 73