memLp

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.memLp

English

A function f belongs to Lp(E, p, μ) exactly when it is almost everywhere strongly measurable and its eLpNorm is finite.

Русский

Функция f принадлежит Lp(E, p, μ) тогда и только тогда, когда она почти везде сильно измерима и eLpNorm(f, p, μ) конечна.

LaTeX

$$f \in L_p(E,p,\mu)$$

Lean4

protected theorem memLp (f : Lp E p μ) : MemLp f p μ :=
  ⟨Lp.aestronglyMeasurable f, f.prop⟩

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

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

Разделы

Аффилиация

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