OptimalInitialLength.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Common initial length of two optimal plans

Only the reference optimizer needs bounded compression. A potential for the average coupling bounds the speed on both optimizers. The Sobolev speed identity and equality of costs make both bounds equalities.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.common_optimal_initial_length line 20