nnHolderNorm_smul — Mathlib

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]

Похожие утверждения