Far-field decay of Newtonian potentials about a general centre

The tail estimates of the Newtonian potential and of its first derivative are stated here for data supported in a closed ball centred at an arbitrary point x₀, rather than at the origin: on the support of the data a far point x with 2 * R ≤ ‖x - x₀‖ satisfies ‖x - y‖ ≥ ‖x - x₀‖ / 2, so the Newtonian kernel bounds of CKN.Foundation.Heat supply the same decay with ‖x - x₀‖ in place of ‖x‖.

These tail estimates are the decay-at-infinity input to the uniqueness half of the Newtonian representation ext:newtonian of the paper, where the difference of two representations is harmonic on all of space and tends to zero in the L^{3/2} average sense.

theorem CKN.pressureNewtonianPotential_tail_bound_centre {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) {x₀ : Foundation.Parabolic.Vec3} {R : ℝ} (hR : 0 < R) (hSupp : tsupport g ⊆ Metric.closedBall x₀ R) {x : Foundation.Parabolic.Vec3} (hx : 2 * R ≤ ‖x - x₀‖) : |pressureNewtonianPotential g x| ≤ 2 * (4 * Real.pi)⁻¹ / ‖x - x₀‖ * ∫ (y : Foundation.Parabolic.Vec3), |g y|

Far-field decay of the Newtonian potential of data supported in the closed ball of radius R about x₀. Decay-at-infinity input to ext:newtonian of the paper, at a general centre.

theorem CKN.pressureNewtonianDerivativePotential_tail_bound_centre {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) {x₀ : Foundation.Parabolic.Vec3} {R : ℝ} (hR : 0 < R) (hSupp : tsupport g ⊆ Metric.closedBall x₀ R) (i : Fin 3) {x : Foundation.Parabolic.Vec3} (hx : 2 * R ≤ ‖x - x₀‖) : |pressureNewtonianDerivativePotential i g x| ≤ 4 * (4 * Real.pi)⁻¹ / ‖x - x₀‖ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3), |g y|

Far-field decay of the first-derivative Newtonian potential of data supported in the closed ball of radius R about x₀. Decay-at-infinity input to ext:newtonian of the paper, at a general centre.