of_le_enorm — Mathlib

English

If hg MemLp g p μ, hf AEStronglyMeasurable f μ and hfg a.e. then MemLp f p μ.

Русский

Если hg MemLp g p μ, f измерима и hfg a.e., то MemLp f p μ.

LaTeX

$$$MemLp g p μ \rightarrow AEStronglyMeasurable f μ \rightarrow (hfg\ a.e.) ⇒ MemLp f p μ.$$$

Lean4

theorem of_le_enorm {f : α → ε} {g : α → ε'} (hg : MemLp g p μ) (hf : AEStronglyMeasurable f μ)
    (hfg : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) : MemLp f p μ :=
  ⟨hf, (eLpNorm_mono_ae' hfg).trans_lt hg.eLpNorm_lt_top⟩

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