OAI/Geometry/RCD/Heat/HeatLevelIntegral.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Time integration of the heat upper-level inequality

Measurability of the cutoff energy follows from lower semicontinuity of the actual Cheeger energy. The differential inequality itself gives its time integrability, without asserting continuity of Sobolev truncation.

  1. theorem OAI.RegularPointCoordinates.measurable_energy_integral line 19
  2. theorem OAI.RegularPointCoordinates.continuous_weighted_square_path line 50
  3. theorem OAI.RegularPointCoordinates.heat_level_cutoff_energy_measurable line 62
  4. theorem OAI.RegularPointCoordinates.heat_level_cutoff_energy_integral line 75