OAI/Geometry/RCD/Transport/LocalSmoothEntropy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite-jet extension of the regularized entropy

On the prescribed bounded nonnegative interval the second derivative is exactly the reciprocal of the value plus epsilon. The two primitives vanish at zero and have the global bounds needed for L² heat calculus.

  1. theorem OAI.RegularPointCoordinates.exists_local_smooth_entropy line 19