of_le_mul' — Mathlib

English

If MemLp g p μ and f is AEStronglyMeasurable and |f| ≤ c|g| a.e., then MemLp f p μ with the bound c.

Русский

Если MemLp g p μ и f измерим по AES и почти везде выполняется |f| ≤ c|g|, тогда MemLp f p μ с границей.

LaTeX

$$$\operatorname{MemLp}(g,p,μ) \land (\text{AEStronglyMeasurable}(f,μ)) \land (∀^{\ast} x, \|f(x)\| ≤ c \|g(x)\|) \Rightarrow \operatorname{MemLp}(f,p,μ)$$$

Lean4

theorem of_le_mul' {f : α → ε} {g : α → ε'} {c : ℝ≥0} (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.coe_lt_top hg.eLpNorm_lt_top⟩

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