OAI/Geometry/RCD/Transport/OptimalTripletCompletion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded geodesic triplet law extends to a compressed optimal plan

The two half plans are constructed from curvature-dimension transport. Sharp quadratic saturation proves their concatenation is geodesic.

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