Far-field geometry for potential decay

Elementary normed-space inequalities used in the far-field estimates for the Newtonian potentials of compactly supported data. Nothing measure-theoretic is involved: each statement is a triangle-inequality estimate on Vec3.

theorem CKN.far_field_norm_sub_ge {x₀ x y : Foundation.Parabolic.Vec3} {R : ℝ} (hx : 2 * R ≤ ‖x - x₀‖) (hy : ‖y - x₀‖ ≤ R) : ‖x - x₀‖ / 2 ≤ ‖x - y‖

On the support of data carried by the closed ball of radius R about x₀, a far point x with 2 * R ≤ ‖x - x₀‖ stays at distance at least ‖x - x₀‖ / 2.

theorem CKN.far_field_sub_ne_zero {x₀ x y : Foundation.Parabolic.Vec3} {R : ℝ} (hR : 0 < R) (hx : 2 * R ≤ ‖x - x₀‖) (hy : ‖y - x₀‖ ≤ R) : x - y ≠ 0

On the support of data carried by the closed ball of radius R about x₀, a far point x with 2 * R ≤ ‖x - x₀‖ is distinct from every such y, so the kernel ‖x - y‖⁻¹ is finite there.

theorem CKN.inv_norm_decay_recentre {h : Foundation.Parabolic.Vec3 → ℝ} {x₀ : Foundation.Parabolic.Vec3} {M R : ℝ} (hM : 0 ≤ M) (hR : 0 < R) (hdecay : ∀ (z : Foundation.Parabolic.Vec3), 2 * R ≤ ‖z - x₀‖ → |h z| ≤ M * ‖z - x₀‖⁻¹) {x : Foundation.Parabolic.Vec3} (hx : 2 * (2 * R + 2 * ‖x₀‖) ≤ ‖x‖) : |h x| ≤ 2 * M * ‖x‖⁻¹

A decay estimate centred at x₀ becomes a decay estimate centred at the origin, at the cost of doubling the constant and the radius.