OAI/Geometry/RCD/Harmonic/RadialBallComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing the auxiliary center radius in radial CD comparison

The small initial ball in the actual transport argument shrinks to the pole. Continuity of the sharp distortion coefficient gives a comparison at every radius, without selecting continuity radii of the measure.

  1. theorem OAI.RegularPointCoordinates.FullCD.ball_contraction_below line 20
  2. theorem OAI.RegularPointCoordinates.FullCD.radial_ball_ratio line 44