integrable_norm_rpow — Mathlib

English

If MemLp f p μ with p > 0 and p ≠ ∞, then ∫ ‖f‖^p dμ is finite; i.e., f ∈ L^p(μ).

Русский

Если MemLp f p μ при p > 0 и p ≠ ∞, то ∫ ‖f‖^p dμ < ∞; то есть f ∈ L^p(μ).

LaTeX

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

Lean4

theorem integrable_norm_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.norm_rpow hp_ne_zero hp_ne_top

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