OAI/Geometry/RCD/Metric/PointedInteriorBallMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive interior mass of weak limits of the actual metric laws

Pointed density supplies an actual source ball. Bishop--Gromov controls its normalized mass uniformly before taking any measured limit.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.metric_law_interior_lower line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.metric_probability_limit_positive line 60