mono'_enorm — Mathlib

English

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

Русский

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

LaTeX

$$$MemLp g p μ \rightarrow AEStronglyMeasurable f μ \rightarrow (∀^{\mathrm{a}} a, \|f(a)\| ≤ g(a)) ⇒ MemLp f p μ.$$$

Lean4

theorem mono'_enorm {f : α → ε} {g : α → ℝ≥0∞} (hg : MemLp g p μ) (hf : AEStronglyMeasurable f μ)
    (h : ∀ᵐ a ∂μ, ‖f a‖ₑ ≤ g a) : MemLp f p μ :=
  MemLp.of_le_enorm hg hf <| h.mono fun _x hx ↦ le_trans hx le_rfl

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