Ball integral of the Newtonian kernel gradient

The gradient ∂ₗN of the Newtonian kernel is bounded by (4π)⁻¹ times the Euclidean-norm power |z|^{-2}, so its integral over the Euclidean ball {y : |y - x| ≤ ρ} is absolutely convergent and scales linearly in ρ: ∫_{|y-x|≤ρ} |∂ₗN(x - y)| ≤ Cρ. The scaling identity ∫_{|z|≤ρ} |z|^{-2} = ρ · ∫_{|z|≤1} |z|^{-2} is obtained from the Haar-measure scaling formula ∫ f(c • z) dz = |c|^{-n} ∫ f(z) dz applied to the indicator of the unit ball. This is an elliptic kernel estimate of the interior estimates of lem:aniso:annulus.

Part 2: integrability and the scaling identity on the Euclidean ball

Part 3: the translation identity and ELb

theorem CIV.ELb_kernel_ball_integral : ∃ (C : ℝ), 0 < C ∧ ∀ (x : CKN.Foundation.Parabolic.Vec3) (ρ : ℝ), 0 < ρ → ∀ (l : Fin 3), MeasureTheory.IntegrableOn (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel l (x - y)) {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ} MeasureTheory.volume ∧ ∫ (y : CKN.Foundation.Parabolic.Vec3) in {y : CKN.Foundation.Parabolic.Vec3 | CKN.Foundation.Parabolic.vec3EuclideanNorm (y - x) ≤ ρ}, |CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel l (x - y)| ≤ C * ρ