integrable_enorm_pow — Mathlib

English

For f: α → ε and p ∈ ℕ, MemLp f p μ implies Integrable (‖f‖^p) μ.

Русский

Для f: α → ε и p ∈ ℕ, MemLp f p μ тогда Integrable(‖f‖^p) μ.

LaTeX

$$$MemLp(f,p,μ) \\Rightarrow Integrable (‖f‖^p) μ$ for natural p.$$

Lean4

theorem integrable_enorm_pow {f : α → ε} {p : ℕ} (hf : MemLp f p μ) (hp : p ≠ 0) :
    Integrable (fun x : α ↦ ‖f x‖ₑ ^ p) μ := by simpa using hf.integrable_enorm_rpow (mod_cast hp) (by simp)

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