OAI/Geometry/SurfaceImmersion/Whitney/ExactCollarRemainderBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform first-derivative control for the retained collar remainders.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.collarInterpolationRemainder line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.collarInterpolationRemainder_smooth line 17
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.collarInterpolationRemainder_bound line 23