norm_setToL1_le_mul_norm' — Mathlib

English

For any scalar c and L1-function f, setToL1 hT (c f) = c · setToL1 hT f.

Русский

Для любого скаляра c и функции f в L1 выполняется setToL1 hT (c f) = c · setToL1 hT f.

LaTeX

$$$setToL1\, h_T\, (c \cdot f) = c \cdot setToL1\, h_T\, f,$$$

Lean4

theorem norm_setToL1_le_mul_norm' (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E) :
    ‖setToL1 hT f‖ ≤ max C 0 * ‖f‖ :=
  calc
    ‖setToL1 hT f‖ ≤ ‖setToL1SCLM α E μ hT‖ * ‖f‖ :=
      ContinuousLinearMap.le_of_opNorm_le _ (norm_setToL1_le_norm_setToL1SCLM hT) _
    _ ≤ max C 0 * ‖f‖ := mul_le_mul (norm_setToL1SCLM_le' hT) le_rfl (norm_nonneg _) (le_max_right _ _)

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