OAI/Geometry/RCD/Heat/HeatGeneratorTimeContinuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Joint positive-time continuity of the actual heat source

A fixed positive-time kernel row transfers continuity of the L2 heat generator to the pointwise source, including its spatial variable.

  1. theorem OAI.RegularPointCoordinates.kernelHeatGeneratorSource_eq_delayed line 20
  2. theorem OAI.RegularPointCoordinates.kernelHeatGeneratorSource_continuousOn_time_space line 38
  3. theorem OAI.RegularPointCoordinates.kernelHeat_log_derivative_continuousOn line 59