The Gaussian subordination identity for the Newtonian kernel

The time integral of the three-dimensional heat kernel is the Newtonian kernel away from its singularity. This identity is the scalar analytic input for the heat-kernel route to the pressure decomposition.

theorem CKN.Foundation.Heat.shift_fderiv_apply_basisVec {u : Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (x y : Parabolic.Vec3) (i : Fin 3) : (fderiv ℝ (fun (z : Parabolic.Vec3) => u (x - z)) y) (basisVec i) = -spatialDeriv u i (x - y)

theorem CKN.Foundation.Heat.heatKernel_laplacian_integral_eq_smooth {u : Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huSupport : HasCompactSupport u) {t : ℝ} (ht : 0 < t) (x : Parabolic.Vec3) : ∫ (y : Parabolic.Vec3), heatKernelLaplacian y t * u (x - y) = heatConv t (spatialLaplacian u) x

Integration by parts moves the heat-kernel Laplacian onto a compactly supported function.

theorem CKN.Foundation.Heat.heatKernel_integral_Ioi {x : Parabolic.Vec3} (hx : x ≠ 0) : ∫ (t : ℝ) in Set.Ioi 0, heatKernel x t = 1 / (4 * Real.pi * Parabolic.vec3EuclideanNorm x)