OAI/Geometry/RCD/Sobolev/SobolevHamiltonJacobiEndpoints.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The correctly scaled action bound between two prescribed times

Rescaling both time and the potential preserves the Hamilton--Jacobi inequality and yields the inverse-time factor in the endpoint cost.

  1. theorem OAI.RegularPointCoordinates.sobolev_hamilton_jacobi_endpoint_comparison line 19