negPart

Mathlib.MeasureTheory.Function.LpSpace.Basic

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

English

The pointwise posPart on Lp agrees a.e. with the posPart of the underlying real-valued representative.

Русский

Точечная posPart на Lp совпадает почти везде с posPart соответствующей вещественной функции.

LaTeX

$$$\\text{coe_posPart}(f) =_{\\mathrm{ae}} \\text{posPart}(f).$$$

Lean4

/-- Negative part of a function in `L^p`. -/
def negPart (f : Lp ℝ p μ) : Lp ℝ p μ :=
  posPart (-f)

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

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

Разделы

Аффилиация

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