neg_part — Mathlib

English

If f ∈ L^p, then the negative part of f, i.e. max(-f,0), also lies in L^p.

Русский

Если f ∈ L^p, то отрицательная часть f, то есть max(-f,0), тоже принадлежит L^p.

LaTeX

$$$\\text{MemLp}(f,p,\\mu) \\Rightarrow \\text{MemLp}(\\max(-f,0),p,\\mu).$$$

Lean4

theorem _root_.MeasureTheory.MemLp.neg_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.neg

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