Constant shifts of weak pressure derivatives

Spatial constants may be subtracted from a pressure slice without changing its weak gradient or its distributional harmonicity. In particular these identities apply to the spatial mean at each fixed time.

theorem CKN.HasWeakPartialDerivOn.sub_const {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {p g : Foundation.Parabolic.Vec3 → ℝ} {k : Fin 3} (hp : MeasureTheory.LocallyIntegrableOn p B MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume) (hpg : HasWeakPartialDerivOn B k p g) (c : ℝ) : HasWeakPartialDerivOn B k (fun (x : Vec 3) => p x - c) g

Subtracting a spatial constant preserves a locally integrable weak partial derivative.

theorem CKN.Foundation.Heat.WeaklyHarmonicOn.sub_const {B : Set Parabolic.Vec3} (hB : IsOpen B) {h : Parabolic.Vec3 → ℝ} (hloc : MeasureTheory.LocallyIntegrableOn h B MeasureTheory.volume) (hh : WeaklyHarmonicOn B h) (c : ℝ) : WeaklyHarmonicOn B fun (x : Parabolic.Vec3) => h x - c

Subtracting a spatial constant preserves distributional harmonicity.