OAI/Geometry/RCD/Transport/HamiltonJacobiPlanBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Hamilton--Jacobi bound on a compressed geodesic plan

The actual squared gradient inequality implies the sharp quadratic transport-action bound, at each time and on the same interior region.

  1. theorem OAI.RegularPointCoordinates.hamilton_jacobi_plan_bound line 19