norm_compLp_le — Mathlib

English

If g is Lipschitz and vanishes at 0, then the Lp-norm of the composition is bounded above by c times the norm of f in Lp.

Русский

Если g Lipschitz и g(0)=0, то норма совместной композиции в Lp не превосходит c умножить на норму f в Lp.

LaTeX

$$norm_compLp_le$$

Lean4

theorem norm_compLp_le (hg : LipschitzWith c g) (g0 : g 0 = 0) (f : Lp E p μ) : ‖hg.compLp g0 f‖ ≤ c * ‖f‖ := by
  -- squeezed for performance reasons
  simpa only [compLp_zero, sub_zero] using hg.norm_compLp_sub_le g0 f 0

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