Heat Kernel Integrable #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.pressure_heat_kernel_integrable
{ψ : Foundation.Parabolic.Vec3 → ℝ}
{y : Foundation.Parabolic.Vec3}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(i : Fin 3)
:
MeasureTheory.Integrable
(fun (p : ℝ × Foundation.Parabolic.Vec3) =>
Foundation.Heat.heatKernel (p.2 - y) p.1 * spatialDeriv (spatialLaplacian ψ) i p.2)
((MeasureTheory.volume.restrict (Set.Ioi 0)).prod MeasureTheory.volume)