Integrability of screened-potential test integrands #
Continuity and compact support give integrability of screened-potential test integrands.
theorem
LiebThirring.integrable_screenedPotentialReal_mul_laplacian
{M : ℕ}
(hM : 1 ≤ M)
(Z : NNReal)
(R : Fin M → Position)
(hR : Function.Injective R)
{f : Position → ℝ}
(hf : ContDiff ℝ 2 f)
(hfc : HasCompactSupport f)
:
MeasureTheory.Integrable (fun (x : Position) => screenedPotentialReal Z R x * Laplacian.laplacian f x)
MeasureTheory.volume