OAI/Geometry/RCD/Metric/AnnularVolumeRatio.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Real-valued sharp annular volume comparison

The coefficient is the radial area density of the negative-curvature model. No model-volume comparison is assumed in obtaining this inequality.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.annular_volume_ratio line 17