OAI/Geometry/RCD/Heat/ScaledHeatIntervalEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrated gradient energy on every interior time interval

The original Sobolev time family and compact spatial test retain their full weighted energy. Its integral is controlled by the actual endpoint values of the continuous small-noise heat limit.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_interval_energy_of_compactness line 30