Kernel All Orders Bounds

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

All-order derivative bounds for the Newtonian kernel

The Newtonian kernel newtonianKernel is homogeneous of degree -1 and of every finite differentiability order away from the origin, so its k-th derivative is homogeneous of degree -(1 + k). Combining this with the compactness of the Euclidean unit sphere gives, for each order k, a constant c with

‖D^k newtonianKernel x‖ ≤ c ‖x‖₂^{-(1 + k)} for x ≠ 0,

and the same statement with exponent -(2 + k) for each first-order kernel ∂_j newtonianKernel. These are the kernel estimates behind cor:CZ-harmonic and the smoothness display eq:har-Ck.

theorem CKN.Foundation.Heat.isOpen_vec3Punctured : IsOpen {z : Parabolic.Vec3 | z ≠ 0}

Space with the origin removed; the Newtonian kernel is smooth there.

theorem CKN.Foundation.Heat.contDiffOn_newtonianKernel (n : ℕ) : ContDiffOn ℝ (↑n) newtonianKernel {z : Parabolic.Vec3 | z ≠ 0}

The Newtonian kernel has every finite differentiability order off the origin.

theorem CKN.Foundation.Heat.differentiableAt_iteratedFDeriv_newtonianKernel (k : ℕ) {x : Parabolic.Vec3} (hx : x ≠ 0) : DifferentiableAt ℝ (iteratedFDeriv ℝ k newtonianKernel) x

Every iterated derivative of the Newtonian kernel is differentiable off the origin.

theorem CKN.Foundation.Heat.continuousOn_iteratedFDeriv_newtonianKernel (k : ℕ) : ContinuousOn (iteratedFDeriv ℝ k newtonianKernel) {z : Parabolic.Vec3 | z ≠ 0}

Every iterated derivative of the Newtonian kernel is continuous off the origin.

theorem CKN.Foundation.Heat.iteratedFDeriv_newtonianKernel_smul (k : ℕ) {r : ℝ} (hr : 0 < r) {x : Parabolic.Vec3} : x ≠ 0 → iteratedFDeriv ℝ k newtonianKernel (r • x) = (r ^ (1 + k))⁻¹ • iteratedFDeriv ℝ k newtonianKernel x

The k-th derivative of the Newtonian kernel is homogeneous of degree -(1 + k).

theorem CKN.Foundation.Heat.exists_norm_iteratedFDeriv_newtonianKernel_le (k : ℕ) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x : Parabolic.Vec3), x ≠ 0 → ‖iteratedFDeriv ℝ k newtonianKernel x‖ ≤ c * (Parabolic.vec3EuclideanNorm x ^ (1 + k))⁻¹

The size of the k-th derivative of the Newtonian kernel away from the origin.

theorem CKN.Foundation.Heat.norm_basisVec_le_one (j : Fin 3) : ‖basisVec j‖ ≤ 1

Each coordinate basis vector has sup norm at most one.

theorem CKN.Foundation.Heat.exists_norm_iteratedFDeriv_newtonianKernel_spatialDeriv_le (j : Fin 3) (k : ℕ) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x : Parabolic.Vec3), x ≠ 0 → ‖iteratedFDeriv ℝ k (spatialDeriv newtonianKernel j) x‖ ≤ c * (Parabolic.vec3EuclideanNorm x ^ (2 + k))⁻¹

The size of the k-th derivative of a first-order Newtonian kernel ∂_j N.