OAI/Geometry/RCD/Sobolev/ScaledHamiltonJacobiGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact scaled equation with its uniform local gradient bound

Locality identifies the gradient of the equation's representative with the independently constructed representative used in the Hamilton bound.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_heat_scaled_equation_gradient line 21