Potential Local Lp Kernel

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

noncomputable def CKN.Foundation.Euclidean.truncatedNewtonianPotentialKernel (R : ℝ) : Parabolic.Vec3 → ℝ

The Newtonian kernel truncated to the ball of radius R about the origin.

Equations

• CKN.Foundation.Euclidean.truncatedNewtonianPotentialKernel R z = if ‖z‖ < R then CKN.Foundation.Heat.newtonianKernel z else 0

theorem CKN.Foundation.Euclidean.measurable_truncatedNewtonianPotentialKernel (R : ℝ) : Measurable (truncatedNewtonianPotentialKernel R)

The truncated Newtonian kernel is measurable.

theorem CKN.Foundation.Euclidean.truncatedNewtonianPotentialKernel_memLp {R s : ℝ} : 0 < R → ∀ (hs : 0 < s) (hs3 : s < 3), MeasureTheory.MemLp (truncatedNewtonianPotentialKernel R) (ENNReal.ofReal s) MeasureTheory.volume

The Newtonian kernel |z|⁻¹ truncated to a ball lies in L^s for every 0 < s < 3.

theorem CKN.Foundation.Euclidean.truncatedNewtonianDerivative_memLp_of_lt_three_halves {R s : ℝ} : 0 < R → ∀ (hs : 0 < s) (hs3 : s < 3 / 2) (i : Fin 3), MeasureTheory.MemLp (truncatedNewtonianDerivative R i) (ENNReal.ofReal s) MeasureTheory.volume

The Newtonian derivative kernel |z|⁻² truncated to a ball lies in L^s for every 0 < s < 3 / 2.