OAI/Geometry/RCD/Heat/LocalSmoothLogarithm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded C² logarithm on a prescribed positive interval

Only the first two derivatives are used in the local weak-Laplacian chain rule. The function and its derivative vanish at zero.

  1. theorem OAI.RegularPointCoordinates.exists_local_smooth_log line 18