OAI/Geometry/RCD/Transport/BoundedOptimalRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded optimal recovery of an arbitrary finite-cost geodesic plan

Cutting off the original plan preserves optimality for the resulting endpoint marginals. All integrable moments converge along the recovery.

  1. theorem OAI.RegularPointCoordinates.bounded_optimal_recovery line 19