OAI/Geometry/RCD/Sobolev/RadialCutoffStrongComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local strong comparison with the original outer-ball normalization

The cutoff is constructed on the physical space. Its comparison with the Euclidean radial weight transfers both the sharp recovery energy and the lower bound, while the exact Poisson identity retains the source errors.

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