OAI/Geometry/RCD/Transport/EndpointDominatedOptimality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Endpoint domination preserves optimality of a path law

This permits a measurable splice to change the paths while keeping its endpoint coupling inside a finite multiple of an existing optimal coupling.

  1. theorem OAI.RegularPointCoordinates.optimal_of_endpoint_domination line 18