Local integrability of the Newtonian fundamental solution
ProvedHunterPDE.Newtonian.locallyIntegrable_fundamentalSolutionintegrationnewtonian-potentialpotential-theory
For every dimension , Hunter’s fundamental solution is locally Lebesgue integrable on : its norm has finite integral over each compact set. The power singularity in dimensions at least three and the logarithmic singularity in dimension two are both integrable. This is the kernel regularity needed to form Newtonian potentials of continuous compactly supported sources.
Preamble
import Definitions.Def_HunterPDE_Newtonian_FundamentalSolution import Mathlib.MeasureTheory.Function.LocallyIntegrable open MeasureTheory HunterPDE.Newtonian
Formal statement
theorem HunterPDE.Newtonian.locallyIntegrable_fundamentalSolution (n : ℕ) (hn : 2 ≤ n) :
LocallyIntegrable (fundamentalSolution n) volume := by sorry
Source
John K. Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, printed p. 33, Section 2.6.1, assertion following Eq. (2.15), and fundamental solution Eq. (2.12); power integrability criterion Example 1.13.