OAI/Geometry/RCD/Metric/HamiltonJacobiDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local pointwise content of the weak Hamilton--Jacobi inequality

A compact radial cutoff and signed-density order retain the original Sobolev gradient and L2 time derivative on a strict interior ball.

  1. theorem OAI.RegularPointCoordinates.hamilton_jacobi_density_of_tests line 20