mem_Lp_of_nnnorm_ae_le_mul — Mathlib

English

If almost everywhere ‖f x‖₊ ≤ c · ‖g x‖₊, then f ∈ Lp E p μ.

Русский

Если почти всюду ‖f x‖₊ ≤ c · ‖g x‖₊, тогда f ∈ Lp.

LaTeX

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

Lean4

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

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