OAI/Geometry/RCD/Heat/LocalLogarithmicGradient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact local weak gradient of a logarithm

The mixed chain rule gives the minimal slope, including at zero-gradient points. Quantitative bounds retain the explicit local lower value.

  1. theorem OAI.RegularPointCoordinates.local_logarithmic_minimalSlope line 19
  2. theorem OAI.RegularPointCoordinates.local_logarithmic_gradient_le line 35