comp_memLp' — Mathlib

English

If a function f: α→E lies in L^p and L is Lipschitz E→F, then L ∘ f lies in L^p.

Русский

Если f: \\alpha \\to E принадлежит L^p, и L: E→F липшицев, то L ∘ f принадлежит L^p.

LaTeX

$$$f: α \\to E, \\ MemLp_p(f) \\Rightarrow MemLp_p(L \\circ f).$$$

Lean4

theorem comp_memLp' (L : E →SL[σ] F) {f : α → E} (hf : MemLp f p μ) : MemLp (L ∘ f) p μ :=
  (L.comp_memLp (hf.toLp f)).ae_eq (EventuallyEq.fun_comp hf.coeFn_toLp _)

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