OAI/Geometry/RCD/Heat/KernelHeatLogarithmicContinuity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual heat bridge continuity equation in logarithmic directions

Compactly supported bounded Sobolev tests see the gradient of the difference of the two local heat logarithms. The global sources are the actual heat generators; no continuity-equation hypothesis is supplied.

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