OAI/Geometry/RCD/Transport/ReducedMidpoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compressed midpoint with the exact reduced-CD lower bound

The original full-CD witness supplies the distortion integral. The actual Rényi maximizer is compressed at the transport-distance capacity. The two plans remain explicit and need not have the same coupling.

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