abs

Mathlib.MeasureTheory.Function.LpOrder

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

English

If f ∈ MemLp, then |f| ∈ MemLp, i.e. taking absolute value preserves membership in Lp.

Русский

Если f ∈ MemLp, то |f| ∈ MemLp; модуль сохраняет принадлежность к Lp.

LaTeX

$$$\text{MemLp}\,f\,p\,\mu \Rightarrow \text{MemLp}\,|f|\,p\,\mu.$$$

Lean4

theorem _root_.MeasureTheory.MemLp.abs {f : α → E} (hf : MemLp f p μ) : MemLp |f| p μ :=
  hf.sup hf.neg

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

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

Разделы

Аффилиация

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