eLpNorm_ofReal — Mathlib

English

If g is MemLp and f is AEStronglyMeasurable with ‖f‖ ≤ g a.e., then MemLp f p μ.

Русский

Если g принадлежит MemLp и f измеримо в сильной мере с почти всюду меньшей нормой, то MemLp f p μ.

LaTeX

$$$MemLp g p μ \Rightarrow AEStronglyMeasurable f μ \Rightarrow (\|f(x)\|_{e} ≤ g(x) \text{ a.e.}) ⇒ MemLp f p μ.$$$

Lean4

/-- `f : α → ℝ` and `ENNReal.ofReal ∘ f : α → ℝ≥0∞` have the same `eLpNorm`.
Usually, you should not use this lemma (but use enorms everywhere.) -/
theorem eLpNorm_ofReal (f : α → ℝ) (hf : ∀ᵐ x ∂μ, 0 ≤ f x) : eLpNorm (ENNReal.ofReal ∘ f) p μ = eLpNorm f p μ :=
  eLpNorm_congr_enorm_ae <| hf.mono fun _x hx ↦ Real.enorm_ofReal_of_nonneg hx

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