OAI/Geometry/SurfaceImmersion/Atlas/LogarithmicCutoffDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic cutoff has a derivative uniformly small after multiplication by the distance from the collar boundary.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.logarithmicCutoff_weighted_derivative line 12