comp_memLp

Mathlib.MeasureTheory.Function.LpSpace.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.comp_memLp

English

If f ∈ L^p(μ;E) and L is a Lipschitz map E→F, then L ∘ f ∈ L^p(μ;F).

Русский

Если f ∈ L^p(μ;E) и L — липшицев переход E→F, то L ∘ f ∈ L^p(μ;F).

LaTeX

$$$f \\in L^p(E,p,μ) \\Rightarrow (L \\circ f) \\in L^p(F,p,μ).$$$

Lean4

theorem comp_memLp (L : E →SL[σ] F) (f : Lp E p μ) : MemLp (L ∘ f) p μ :=
  (Lp.memLp (L.compLp f)).ae_eq (L.coeFn_compLp' f)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru