OAI/Geometry/RCD/Sobolev/RadialCutoffEnergyTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Replacing a physical radial cutoff by its Euclidean image weight

Only an interior gradient bound is used. Both cutoffs vanish outside that interior ball once the measured-approximation error is small.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.radial_cutoff_energy_error_tendsto line 19