OAI/Geometry/RCD/Heat/HeatCutoffIntegral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Time-integrated local heat energy

The error remains a space-time integral against the squared cutoff gradient. The positive starting time avoids imposing Sobolev regularity on the datum.

  1. theorem OAI.RegularPointCoordinates.integral_energy_inequality line 17
  2. theorem OAI.RegularPointCoordinates.heat_weighted_square_continuous line 35
  3. theorem OAI.RegularPointCoordinates.heatTail_continuous line 48
  4. theorem OAI.RegularPointCoordinates.heat_cutoff_error_continuous line 54
  5. theorem OAI.RegularPointCoordinates.heat_cutoff_energy_integral line 70