OAI/Geometry/RCD/Metric/SquaredDistanceInequality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The squared-distance Laplacian inequality from actual CD contraction

Contract normalized volume in a ball toward its center. The explicit density bound controls nonnegative test integrals; the uniform radial first variation identifies their infinitesimal change with the energy pairing.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.squaredDistance_laplacian_test line 23