OAI/Geometry/RCD/Transport/DiracTransportCost.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every coupling to a Dirac measure has the same transport cost

This identifies the limiting radial plan as optimal without retaining an extra optimality assumption in the concentration argument.

  1. theorem OAI.RegularPointCoordinates.transportCost_eq_moment_of_dirac line 18
  2. theorem OAI.RegularPointCoordinates.isOptimalCoupling_of_dirac line 33