memLp_comp_iff_of_antilipschitz — Mathlib

English

If L is a Lipschitz map, then composing with L preserves MemLp membership; more strongly, there is a Lipschitz bound for the composition in Lp.

Русский

Если L — липшицева функция, композиция с L сохраняет принадлежность к MemLp; более того, есть ограничение по липшицу для композиции в Lp.

LaTeX

$$continuousLinearMap_comp$$

Lean4

theorem memLp_comp_iff_of_antilipschitz {α E F} {K K'} [MeasurableSpace α] {μ : Measure α} [NormedAddCommGroup E]
    [NormedAddCommGroup F] {f : α → E} {g : E → F} (hg : LipschitzWith K g) (hg' : AntilipschitzWith K' g)
    (g0 : g 0 = 0) : MemLp (g ∘ f) p μ ↔ MemLp f p μ :=
  ⟨fun h => h.of_comp_antilipschitzWith hg.uniformContinuous hg' g0, fun h => hg.comp_memLp g0 h⟩

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