const_smul_mem_Lp — Mathlib

English

Scalar multiplication by c on an Lp-function is again Lp.

Русский

Умножение на константу c функцию из Lp снова принадлежит Lp.

LaTeX

$$$c \in 𝕜 \;\Rightarrow\; c \cdot f \in Lp\; E\; p\; μ$$$

Lean4

theorem const_smul_mem_Lp (c : 𝕜) (f : Lp E p μ) : c • (f : α →ₘ[μ] E) ∈ Lp E p μ :=
  by
  rw [mem_Lp_iff_eLpNorm_lt_top, eLpNorm_congr_ae (AEEqFun.coeFn_smul _ _)]
  exact eLpNorm_const_smul_le.trans_lt <| (by finiteness)

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