OAI/Geometry/RCD/Heat/ScaledHeatGradientTimeDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact gradient energy bounded by ordinary time derivatives

The continuous small-noise limit has absolutely continuous compact spatial pairings. Their almost-everywhere derivatives replace the distributional time derivative in the weighted Hamilton--Jacobi inequality.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_gradient_time_derivative_of_compactness line 28