OAI/Geometry/RCD/Coordinates/RegularMetricLimitMeasure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized volume law on a regular metric limit

The measure is constructed from the original Hausdorff measures and measurable pointed maps. Its exact interior ball masses require no RCD structure on the target metric space.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_metric_limit_measure line 23