OAI/Geometry/RCD/Coordinates/BoundedRegularGramEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A local mixed Gram for the actual bounded regular test

Only the test is cut off. The two prescribed full positive Bochner measures are retained, so the estimate uses their original mass on the smaller ball.

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