OAI/Geometry/SurfaceImmersion/Correction/SpecialPointCorrection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Small affine bumps prescribe the vertical derivative near an isolated special point.

  1. abbrev OAI.ClosedSurfaceR4.TransverseSmallFunction.Base line 12
  2. def OAI.ClosedSurfaceR4.TransverseSmallFunction.pointCorrection line 14
  3. lemma OAI.ClosedSurfaceR4.TransverseSmallFunction.pointCorrection_smooth line 17
  4. lemma OAI.ClosedSurfaceR4.TransverseSmallFunction.pointCorrection_support line 21
  5. lemma OAI.ClosedSurfaceR4.TransverseSmallFunction.pointCorrection_compact line 26
  6. lemma OAI.ClosedSurfaceR4.TransverseSmallFunction.pointCorrection_derivative line 31
  7. lemma OAI.ClosedSurfaceR4.TransverseSmallFunction.pointCorrection_abs_le line 44
  8. theorem OAI.ClosedSurfaceR4.TransverseSmallFunction.exists_special_point_correction line 63