OAI/Geometry/SurfaceImmersion/Atlas/PhaseExteriorControl.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exterior C2 control in the actual nonlinear phase chart, including the closure of the exterior where its boundary is glued.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseRealChartMap_eventuallyEq line 23
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_profile_eq_on_exterior_closure line 45
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_real_profile_correction_bound line 71
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_exterior_profile_bound_closure line 87