English
Let g: E → F be c-Lipschitz with g(0) = 0. Then the map sending f ∈ L^p(μ;E) to g ∘ f ∈ L^p(μ;F) is Lipschitz on L^p with constant c (provided 1 ≤ p).
Русский
Пусть g: E → F гладко-ограничена Lipschitz с константой c и g(0) = 0. Тогда отображение, отправляющее f ∈ L^p(μ;E) в g ∘ f ∈ L^p(μ;F), является Lipschitz-с отображением на L^p с константой c (при 1 ≤ p).
LaTeX
$$$1 \\le p \\le \\infty \\;\\wedge\\; g: E \\to F \\\\text{ является } c\\text{-Lipshitz с } g(0)=0 \\\\Rightarrow \\\\forall f,h \\in L^p(E,p,\\mu): \\\\|g\\circ f - g\\circ h\\|_{L^p(\\mu)} \\le c\\|f-h\\|_{L^p(\\mu)}.$$$
Lean4
theorem lipschitzWith_compLp [Fact (1 ≤ p)] (hg : LipschitzWith c g) (g0 : g 0 = 0) :
LipschitzWith c (hg.compLp g0 : Lp E p μ → Lp F p μ) :=
-- squeezed for performance reasons
LipschitzWith.of_dist_le_mul fun f g => by simp only [dist_eq_norm, norm_compLp_sub_le]
