OAI/Geometry/RCD/Transport/RecoveryLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual noncompact recovery limit

The bounded reduced-CD plans converge to an optimal geodesic plan. Every bounded length window keeps its uniform compression constant. This does not yet assert passage of the reduced entropy inequality to the limit.

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