eLpNorm_const_smul_le' — Mathlib

English

Let c be a scalar and f a function. Then the extended-Lp norm of the scalar multiple c · f is no larger than the norm of c times the extended-Lp norm of f:

Русский

Пусть c — скаляр, а f — функция. Тогда расширенная норма Lp от произведения c · f не превосходит ‖c‖ₑ · eLpNorm(f):

LaTeX

$$$\\\\| c f \\\\|_{L^p(\\\\mu)} \\\\le \\\\|c\\\\|_e \\\\, \\\\| f \\\\|_{L^p(\\\\mu)}$$$

Lean4

theorem eLpNorm_const_smul_le' : eLpNorm (c • f) p μ ≤ ‖c‖ₑ * eLpNorm f p μ :=
  eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul' (Eventually.of_forall fun _ => le_of_eq (enorm_smul ..)) _

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