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 μ for p ∈ ℕ, then Integrable (‖f‖^p) μ.

Русский

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

LaTeX

$$MemLp(f,p.cast,μ) ⇒ Integrable (‖f‖^p) μ$$

Lean4

theorem integrable_norm_pow' [IsFiniteMeasure μ] {f : α → β} {p : ℕ} (hf : MemLp f p μ) :
    Integrable (fun x : α => ‖f x‖ ^ p) μ := by simpa using hf.integrable_norm_rpow'

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

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

Разделы

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

Аффилиация

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