continuousLinearMap_comp — Mathlib

English

Under stronger hypotheses, MemLp(f,p,μ) is equivalent to MemLp(g∘f,p,μ) when g is uniformly continuous and antilipschitz.

Русский

При более сильных условиях MemLp(f,p,μ) эквивалентно MemLp(g∘f,p,μ), если g равномерно непрерывна и анлипшиц.

LaTeX

$$of_comp_antilipschitzWith$$

Lean4

theorem continuousLinearMap_comp [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : α → E}
    (h_Lp : MemLp f p μ) (L : E →L[𝕜] F) : MemLp (fun x ↦ L (f x)) p μ :=
  LipschitzWith.comp_memLp L.lipschitz (by simp) h_Lp

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