OAI/Geometry/RCD/Heat/HeatLocalEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local space-time energy of heat upper levels

Cutoff locality restricts the error to its outer support. A plateau on the inner set gives the local L² mass at the final time.

  1. theorem OAI.RegularPointCoordinates.continuous_setIntegral_sq_path line 21
  2. theorem OAI.RegularPointCoordinates.cutoff_L2_norm_sq_le_setIntegral line 44
  3. theorem OAI.RegularPointCoordinates.heat_level_error_continuous line 70
  4. theorem OAI.RegularPointCoordinates.heat_level_local_energy line 90