OAI/Geometry/RCD/Metric/PointedProbabilityCompactness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compactness of the actual laws of metric approximation maps

No measured approximation or identification of the limiting measure is assumed. The laws retain the original ball and its exact normalization.

  1. theorem OAI.RegularPointCoordinates.normalizedBallPushforward_supported line 21
  2. theorem OAI.RegularPointCoordinates.pointed_probability_subsequence line 45
  3. theorem OAI.RegularPointCoordinates.pointed_probability_limit_support line 80