pos_part — Mathlib

English

Positivity-preserving operator on Lp: applying max(·,0) to an Lp function yields another Lp function.

Русский

Оператор, сохраняющий неотрицательность, на Lp: применение max(·,0) к функции в Lp выдает другую функцию в Lp.

LaTeX

$$$\\text{posPart}(f) = f^{+} = \\max(f,0) \\in L^p(\\mu).$$$

Lean4

theorem _root_.MeasureTheory.MemLp.pos_part {f : α → ℝ} (hf : MemLp f p μ) : MemLp (fun x => max (f x) 0) p μ :=
  lipschitzWith_pos_part.comp_memLp (max_eq_right le_rfl) hf

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