OAI/Geometry/RCD/Transport/PointedOptimalLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Optimality of the actual Euclidean endpoint limit

The proof transfers the original optimal potentials, preserves their exact contact integral, and tests every coupling of the limiting marginals.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.pointed_optimal_limit line 20