Heat Kernel Fundamental Solution

Supporting estimates for the Navier–Stokes development.

theorem CKN.Foundation.Heat.heatKernelPlusDistribution_fundamentalSolution : (Distribution.lineDerivCLM (0, 1)) heatKernelPlusDistribution - ∑ i : Fin 3, (Distribution.lineDerivCLM (basisVec i, 0)) ((Distribution.lineDerivCLM (basisVec i, 0)) heatKernelPlusDistribution) = Distribution.delta 0

The causal heat kernel is a fundamental solution of the heat operator, as a distribution on the ordinary product space ℝ³ × ℝ (paper label ext:heat-kernel).