OAI/Geometry/SurfaceImmersion/Atlas/AtlasSecondFormMargin.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single positive second-form margin for all fixed atlas supports and all sufficiently C2-close maps.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.compact_read_secondForm_C2_margin line 18
  2. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.MetricGoodPhaseData.uniform_secondForm_C2_margin line 58