lipschitzWith_pos_part — Mathlib

English

The real-valued Lipschitz map x ↦ max(x,0) induces a Lipschitz operator on L^p by post-composition with real-valued functions.

Русский

Гладкая по Липшицу функция, действующая на вещественных числах, порождает липшицев оператор на L^p через композицию.

LaTeX

$$$\\text{posPart}: L^p(\\mathbb{R},p,\\mu) \\to L^p(\\mathbb{R},p,\\mu)$ is 1-Lipschitz; i.e. \\|\\text{posPart}(f) - \\text{posPart}(h)\\|_p ≤ \\|f-h\\|_p.$$$

Lean4

theorem lipschitzWith_pos_part : LipschitzWith 1 fun x : ℝ => max x 0 :=
  LipschitzWith.id.max_const _

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