OAI/Geometry/RCD/Heat/HeatCylinderEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A time-cutoff Caccioppoli bound for the actual heat flow

Choosing the initial slice in an earlier time interval replaces its mass by the space-time mass. The same bound controls every later slice and the cutoff energy integrated over the later cylinder.

  1. theorem OAI.RegularPointCoordinates.exists_time_le_integral_mean line 18
  2. theorem OAI.RegularPointCoordinates.heat_level_cylinder_energy line 38