OAI/Geometry/RCD/Metric/SquaredDistanceFunctionalBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-mass bound for the squared-distance distribution

A cutoff in the ball of triple radius majorizes every nonnegative test in the original ball. Positivity on the larger ball gives a uniform mass bound.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.squaredDistance_functional_bound line 21