Potential decay estimates

Far-field derivative bounds and the resulting decay of the scalar potential.

theorem CKN.Leray.associatedPressureNewtonianPotential_timePartial {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartial (associatedPressureNewtonianPotential g) z = associatedPressureNewtonianPotential (fun (q : Foundation.Parabolic.Vec3 × ℝ) => timePartial (have this := g; this) q) z

The Newtonian potential commutes with time differentiation for smooth, compactly supported sources, as used in lem:helmholtz-test.

theorem CKN.Leray.associatedPressureHelmholtzScalarPotential_decay {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) : RieszPressurePotentialDecay (associatedPressureHelmholtzScalarPotential φ)

The scalar Newtonian Helmholtz potential has all the spatial decay data required to invoke the proved Riesz pressure duality result.