norm_smul_le — Mathlib

English

Smul by a scalar commutes with lpPairing: holder(r,B, c f, g) = c holder(r,B,f,g).

Русский

Умножение на скаляр в первом аргументе сохраняется: holder(r,B,c f,g) = c holder(r,B,f,g).

LaTeX

$$$\\mathrm{holder}(r,B,c\\cdot f,g) = c\\cdot \\mathrm{holder}(r,B,f,g).$$$

Lean4

protected theorem norm_smul_le (f : Lp 𝕜 p μ) (g : Lp E q μ) : ‖f • g‖ ≤ ‖f‖ * ‖g‖ :=
  by
  simp only [Lp.norm_def, ← ENNReal.toReal_mul]
  refine ENNReal.toReal_mono (by finiteness) ?_
  rw [eLpNorm_congr_ae (coeFn_lpSMul f g)]
  exact eLpNorm_smul_le_mul_eLpNorm (Lp.aestronglyMeasurable g) (Lp.aestronglyMeasurable f)

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