English
For q > 0, scaling the function scales the eLpNorm' by the modulus of the scalar: eLpNorm'(c f)_{q} = |c|_e · eLpNorm'(f)_{q}.
Русский
Для q > 0 однородность: eLpNorm'(c f)_{q} = |c|ₑ · eLpNorm'(f)_{q}.
LaTeX
$$$$eLpNorm'(c \\cdot f)_{q} \\\\;= \\\\; \\|c\\|_e \\, eLpNorm'(f)_{q} \qquad (q > 0).$$$$
Lean4
theorem eLpNorm'_const_smul {f : α → F} (c : 𝕜) (hq_pos : 0 < q) : eLpNorm' (c • f) q μ = ‖c‖ₑ * eLpNorm' f q μ :=
by
obtain rfl | hc := eq_or_ne c 0
· simp [eLpNorm'_eq_lintegral_enorm, hq_pos]
refine le_antisymm (eLpNorm'_const_smul_le hq_pos) <| ENNReal.mul_le_of_le_div' ?_
simpa [enorm_inv, hc, ENNReal.div_eq_inv_mul] using eLpNorm'_const_smul_le (c := c⁻¹) (f := c • f) hq_pos