Neg

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_neg (p q : ℝ) (f : ParabolicPoint → ℝ) : (morreyNorm p q fun (z : ParabolicPoint) => -f z) = morreyNorm p q f

Negation leaves the parabolic Morrey seminorm invariant.

theorem CKN.Foundation.Parabolic.Morrey.morreyNorm_abs (p q : ℝ) (f : ParabolicPoint → ℝ) : (morreyNorm p q fun (z : ParabolicPoint) => |f z|) = morreyNorm p q f

Absolute value leaves the parabolic Morrey seminorm invariant.