OAI/Geometry/RCD/Heat/KernelHeatTimeDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pointwise positive-time differentiation of the actual kernel heat flow

A fixed positive-time L2 kernel row turns the L2 heat derivative into a pointwise derivative. No almost-everywhere choice in the time variable is needed.

  1. theorem OAI.RegularPointCoordinates.kernelHeat_add line 21
  2. theorem OAI.RegularPointCoordinates.kernelHeat_weakLaplacian_hasDerivAt line 27