OAI/Geometry/RCD/Heat/HeatGammaEnergyEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A quantitative energy bound for heat energy densities

After absorbing the mixed term, the estimate uses the L² norm of the Laplacian, with no derivatives or amplitude bound on that Laplacian.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_gamma_energy_estimate line 20