OAI/Geometry/RCD/Heat/KernelHeatSourceLower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pointwise lower bounds for the actual continuous heat source

The source has its own positive-time continuous representative. Full support therefore removes the exceptional spatial set at every prescribed time.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.kernelHeat_source_lower line 23