The force-pressure gradient of the zero force

The pointwise force-pressure gradient forcePressureGradientFunction vanishes identically on the zero coordinate field, as used for (R3) of thm:regularised with zero forcing.

theorem CKN.Leray.forcePressureGradientFunction_zero (hf : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => 0) 2 MeasureTheory.volume) : forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => 0) hf = fun (x : Foundation.Parabolic.Vec3) => 0

The pointwise force-pressure gradient of the zero coordinate field is identically zero.