OAI/Geometry/RCD/Transport/SobolevHamiltonJacobiPlan.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Endpoint comparison from the Sobolev Hamilton--Jacobi inequality

The temporal difference is differentiated in L2. The spatial difference uses a fixed Sobolev function and the test-plan slope bound. A one-sided mean-value theorem combines them without evaluating null sets on a diagonal.

  1. theorem OAI.RegularPointCoordinates.sobolev_hamilton_jacobi_plan_comparison line 21