Kernels

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

theorem CKN.Foundation.Harmonic.Commutator.newtonianKernel_eq_scaled (m j l : Fin 3) (x : Vec 3) : newtonianKernel m j l x = -(4 * Real.pi)⁻¹ * inverseThirdFormula m j l x

theorem CKN.Foundation.Harmonic.Commutator.newtonianKernel_size_bound {x : Vec 3} (hx : x ≠ 0) (m j l : Fin 3) : |newtonianKernel m j l x| ≤ 24 / (4 * Real.pi) * vecEuclideanNorm x ^ (-4)

theorem CKN.Foundation.Harmonic.Commutator.newtonianKernel_eq_iterated_spatialDeriv {x : Vec 3} (hx : x ≠ 0) (m j l : Fin 3) : spatialDeriv (spatialDeriv (spatialDeriv newtonianPotential l) j) m x = newtonianKernel m j l x