posPart — Mathlib

English

Negative part of an Lp function is defined via the positive part of its negation: negPart(f) = posPart(-f).

Русский

Отрицательная часть функции в Lp определяется через положительную часть её отрицания: negPart(f) = posPart(-f).

LaTeX

$$$\\text{negPart}(f) = \\text{posPart}(-f).$$$

Lean4

/-- Positive part of a function in `L^p`. -/
def posPart (f : Lp ℝ p μ) : Lp ℝ p μ :=
  lipschitzWith_pos_part.compLp (max_eq_right le_rfl) f

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