OAI/Geometry/RCD/Metric/ConcentratedTimeLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Concentration of radial transport at a prescribed time

Compactness preserves the chosen-time density bound while the final endpoint concentrates. No density bound at the pole is required.

  1. theorem OAI.RegularPointCoordinates.exists_concentrated_time_limit line 21