OAI/Geometry/RCD/Heat/KernelHeatLogarithmicEquation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local logarithmic heat equation from the actual semigroup

On any compact region where the heat value is positive, the logarithm has a Sobolev extension with L² Laplacian. Its pointwise time derivative agrees almost everywhere with that Laplacian plus its squared gradient.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.kernelHeat_logarithmic_equation line 25