OAI/Geometry/RCD/Metric/ModelVolumeComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The required model Bishop--Gromov comparison from the actual CD condition

The proof integrates the annular transport inequality. The preliminary radial comparison supplies absolute continuity and null spheres, so this does not assume any instance of model-volume monotonicity.

  1. theorem OAI.RegularPointCoordinates.comparisonModelVolume_sinh_normalization line 16
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.negative_model_ballVolumeComparison line 34
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_model_ballVolumeComparison line 62