Constant shifts of a weak spatial derivative

The pressure of a suitable weak solution is determined only up to a function of time. Subtracting such a function leaves every weak spatial derivative of the pressure slice unchanged, so a slice estimate proved for the shifted pressure is an estimate for the original pressure gradient.

theorem CKN.Core.Step4.hasWeakPartialDerivOn_const {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) (c : ℝ) (k : Fin 3) : HasWeakPartialDerivOn B k (fun (x : Vec 3) => c) fun (x : Vec 3) => 0

A constant function has vanishing weak spatial derivative.

theorem CKN.Core.Step4.hasWeakPartialDerivOn_add_const {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {u g : Foundation.Parabolic.Vec3 → ℝ} {k : Fin 3} (hu : MeasureTheory.LocallyIntegrableOn u B MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume) (hug : HasWeakPartialDerivOn B k u g) (c : ℝ) : HasWeakPartialDerivOn B k (fun (x : Vec 3) => u x + c) g

Adding a constant to the function leaves a weak spatial derivative unchanged.

theorem CKN.Core.Step4.hasWeakPartialDerivOn_sub_const {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {u g : Foundation.Parabolic.Vec3 → ℝ} {k : Fin 3} (hu : MeasureTheory.LocallyIntegrableOn u B MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume) (hug : HasWeakPartialDerivOn B k u g) (c : ℝ) : HasWeakPartialDerivOn B k (fun (x : Vec 3) => u x - c) g

Subtracting a constant from the function leaves a weak spatial derivative unchanged.