mem_Lp_of_nnnorm_ae_le — Mathlib

English

If a.e. bound holds between a measureable function and g, then membership in Lp follows.

Русский

Если существует ae-граница между функциями, то принадлежность к Lp сохраняется.

LaTeX

$$$(\forall^{\mathrm{ae}} x, \|f(x)\|_+ ≤ \|g(x)\|_+) \Rightarrow f ∈ Lp\, E\, p\, μ$$$

Lean4

theorem mem_Lp_of_nnnorm_ae_le {f : α →ₘ[μ] E} {g : Lp F p μ} (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) : f ∈ Lp E p μ :=
  mem_Lp_iff_memLp.2 <| MemLp.of_le (Lp.memLp g) f.aestronglyMeasurable h

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