English
If g is Lipschitz and vanishes at 0, then the map f ↦ g∘f sends MemLp into MemLp with a bound on the norm growth given by the Lipschitz constant.
Русский
Если g勉 Lipschitz и обращается в нуль, то отображение f ↦ g∘f переводит MemLp в MemLp с ограничением роста нормы, заданным константой липшицевости.
LaTeX
$$norm_compLp_sub_le$$
Lean4
theorem comp_memLp {α E F} {K} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F]
{f : α → E} {g : E → F} (hg : LipschitzWith K g) (g0 : g 0 = 0) (hL : MemLp f p μ) : MemLp (g ∘ f) p μ :=
have : ∀ x, ‖g (f x)‖ ≤ K * ‖f x‖ := fun x ↦ by
-- TODO: add `LipschitzWith.nnnorm_sub_le` and `LipschitzWith.nnnorm_le`
simpa [g0] using hg.norm_sub_le (f x) 0
hL.of_le_mul (hg.continuous.comp_aestronglyMeasurable hL.1) (Eventually.of_forall this)
