OAI/Geometry/RCD/Harmonic/RadialTime.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Radial plans with the small-time CD density bound

The terminal laws are actual normalized balls shrinking to the pole. The one-sided source bound remains uniform and passes to the limit.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_radial_time_plan line 20