OAI/Geometry/RCD/Heat/ScaledHeatTimeAverageEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted gradient control for the actual time-averaged heat limit

The same Sobolev time family yields continuous Sobolev-valued averages. Their weighted energy is bounded by the actual endpoint difference of compact spatial pairings, for every nonnegative compact Lipschitz test.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_time_average_energy_of_compactness line 24