Kernel All Orders Smooth

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

Smoothness and scaling of the Newtonian kernel away from the origin

The kernel newtonianKernel of cor:CZ-harmonic is a constant multiple of a negative real power of the quadratic form q, hence of every finite differentiability order away from the origin, and it is homogeneous of degree -1 under dilations.

theorem CKN.Foundation.Heat.newtonianKernel_eq_q_rpow (z : Parabolic.Vec3) : newtonianKernel z = (4 * Real.pi)⁻¹ * q z ^ (-1 / 2)

The Newtonian kernel as a real power of the quadratic form q.

theorem CKN.Foundation.Heat.contDiffAt_newtonianKernel (n : ℕ) {x : Parabolic.Vec3} (hx : x ≠ 0) : ContDiffAt ℝ (↑n) newtonianKernel x

The Newtonian kernel has every finite differentiability order away from the origin.

theorem CKN.Foundation.Heat.newtonianKernel_smul_left {r : ℝ} (hr : 0 < r) (x : Parabolic.Vec3) : newtonianKernel (r • x) = r⁻¹ * newtonianKernel x

Homogeneity of degree -1 of the Newtonian kernel.