Newtonian Kernel Integrability

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Heat.locallyIntegrable_newtonianKernel : MeasureTheory.LocallyIntegrable newtonianKernel MeasureTheory.volume

The Newtonian kernel newtonianKernel z = 1/(4π|z|₂) is locally integrable with respect to Lebesgue measure on ℝ³.

theorem CKN.Foundation.Heat.locallyIntegrable_newtonianKernel_sub (x : Parabolic.Vec3) : MeasureTheory.LocallyIntegrable (fun (y : Parabolic.Vec3) => newtonianKernel (x - y)) MeasureTheory.volume

For any x : ℝ³, the translated kernel y ↦ newtonianKernel (x - y) is also locally integrable with respect to Lebesgue measure.