OAI/Geometry/RCD/Transport/ReducedRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual compressed reduced-CD recovery of an unbounded optimal plan

The fixed endpoint capacity controls each fixed length window independently of the radii of the bounded recovery. The full transport costs converge.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.reduced_recovery_sequence line 20