OAI/Geometry/RCD/Coordinates/RegularQuadraticTransportPaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absolute squared-distance path errors near every regular point

All Poisson, source, cutoff and second-order data are constructed internally. The remaining hypotheses describe only the given compressed optimal plans.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_quadratic_transport_paths line 21