mem_Lp_of_ae_le_mul — Mathlib

English

If almost everywhere bound on nnnorm holds, then f belongs to Lp.

Русский

Если почти всюду выполняется ограничение по nnnorm, значит f ∈ Lp.

LaTeX

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

Lean4

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

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