integrable_enorm_rpow — Mathlib

English

If f is in L^p(μ) for some p = ℝ≥0∞ with 0 < p < ∞, then the function x ↦ ‖f(x)‖^p is integrable over μ.

Русский

Если функция f принадлежит L^p(μ) при 0 < p < ∞, то x ↦ ‖f(x)‖^p интегрируема по μ.

LaTeX

$$$\\text{If } f ∈ L^p(μ) \\text{ with } 0 < p < ∞, \\text{ then } ∫_α ‖f(x)‖^p \\, dμ(x) < ∞.$$$

Lean4

theorem integrable_enorm_rpow {f : α → ε} {p : ℝ≥0∞} (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    Integrable (fun x : α => ‖f x‖ₑ ^ p.toReal) μ :=
  by
  rw [← memLp_one_iff_integrable]
  exact hf.enorm_rpow hp_ne_zero hp_ne_top

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