English
For a scalar c and MemHolder r f, the Holder norm scales as nnHolderNorm r (c • f) = |c|₊ · nnHolderNorm r f.
Русский
Для скаляра c и MemHolder r f выполняется: nnHolderNorm r (c • f) = |c|₊ · nnHolderNorm r f.
LaTeX
$$$nnHolderNorm\, r\; (c \cdot f) = \lVert c \rVert_{+} \cdot nnHolderNorm\, r\; f$$$
Lean4
theorem nnHolderNorm_smul {α} [NormedRing α] [Module α Y] [NormSMulClass α Y] (hf : MemHolder r f) (c : α) :
nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f := by
rw [← ENNReal.coe_inj, coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm, hf.smul.coe_nnHolderNorm_eq_eHolderNorm,
eHolderNorm_smul]