integrable_norm_pow

Mathlib.MeasureTheory.Function.L1Space.Integrable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MemLp.integrable_norm_pow

← MathLib Explorer

English

If MemLp f p μ with p ∈ ℕ, then Integrable (‖f‖^p) μ.

Русский

Если MemLp f p μ для p ∈ ℕ, то Integrable(‖f‖^p) μ.

LaTeX

$$$MemLp(f,p.cast,μ) \\Rightarrow Integrable (\\|f\\|^p) μ$.$$

Lean4

theorem integrable_norm_pow {f : α → β} {p : ℕ} (hf : MemLp f p μ) (hp : p ≠ 0) :
    Integrable (fun x : α => ‖f x‖ ^ p) μ := by simpa using hf.integrable_norm_rpow (mod_cast hp) (by simp)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru