OAI/Geometry/RCD/Transport/TransportCostEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local energy bounds with the actual transport cost

The mean endpoint variation is controlled by the quadratic transport cost, rather than the largest displacement of the plan. The energy is restricted to the region containing its time marginals.

  1. theorem OAI.RegularPointCoordinates.integral_mul_square_le line 18
  2. theorem OAI.RegularPointCoordinates.testPlan_local_flux_square_le line 45
  3. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_cost_energy line 64