OAI/Geometry/RCD/Metric/ConcentratingProbability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weak convergence when a probability concentrates at a point

Used for the second endpoint of radial transport. The estimate uses only continuity at the pole and probability mass one, and retains the original measures throughout the limit.

  1. theorem OAI.RegularPointCoordinates.probability_tendsto_dirac_of_radius line 19