OAI/Geometry/RCD/Transport/AnnularTransportComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Annular volume contraction from the actual CD transport inequality

The initial endpoint is a small ball about the pole; the final endpoint is an annulus. Retaining the radial distortion, rather than its coarse exponential lower bound, is the step needed for model volume comparison.

  1. theorem OAI.RegularPointCoordinates.FullCD.annular_contraction line 19
  2. theorem OAI.RegularPointCoordinates.FullCD.ball_contraction_with_center_error line 84