of_le_mul — Mathlib

English

If f is MemLp, then c · f is MemLp with the same p, for any scalar c.

Русский

Если f ∈ MemLp, то c · f ∈ MemLp с тем же p для любого скалярного множителя c.

LaTeX

$$$\operatorname{MemLp}(f,p,μ) \Rightarrow \operatorname{MemLp}(c \cdot f, p, μ)$$$

Lean4

theorem of_le_mul {f : α → E} {g : α → F} {c : ℝ} (hg : MemLp g p μ) (hf : AEStronglyMeasurable f μ)
    (hfg : ∀ᵐ x ∂μ, ‖f x‖ ≤ c * ‖g x‖) : MemLp f p μ :=
  ⟨hf,
    (eLpNorm_le_mul_eLpNorm_of_ae_le_mul hfg p).trans_lt <| ENNReal.mul_lt_top ENNReal.ofReal_lt_top hg.eLpNorm_lt_top⟩
    -- TODO: eventually, deprecate and remove the nnnorm version

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