OAI/Geometry/RCD/Coordinates/ComparableRadiusSplitting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Full transformed splitting estimates at comparable radii

This is the analytic one-step part of transformation. The all-scale geometric propagation is not assumed or asserted here.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.interior_radius_splitting line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.comparable_radius_splitting line 131