OAI/Geometry/RCD/Heat/HeatLevelEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Localized heat energy above a level

The squared positive part has an L² derivative at every level. Locality identifies its square-cutoff test with the original heat equation, so the local energy estimate holds for every nonnegative level.

  1. theorem OAI.RegularPointCoordinates.heat_level_cutoff_norm_hasDerivAt line 22
  2. theorem OAI.RegularPointCoordinates.heat_level_cutoff_energy_differential line 47