OAI/Geometry/RCD/Heat/ScaledHeatLipschitzEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual heat-limit energy inequality for all compact Lipschitz tests

No weak Laplacian is required of the spatial test. Positive heat-core approximation and exact source locality extend the same interval bound.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_lipschitz_energy_of_compactness line 22