Quantitative scalar multiplication in Morrey seminorms

The absolute scalar factor is retained in the bound, including when the scalar vanishes or the unscaled seminorm is infinite.

theorem CKN.Core.Endgame.morreyNorm_const_mul_le {P τ : ℝ} (hP : 0 < P) (c : ℝ) (f : Foundation.Parabolic.ParabolicPoint → ℝ) : (Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) => c * f z) ≤ ENNReal.ofReal |c| * Foundation.Parabolic.Morrey.morreyNorm P τ f

Multiplication by a real constant scales the Morrey seminorm by at most its absolute value. No measurability or finiteness assumptions are needed.