compLp — Mathlib

English

Composition with a Lipschitz linear operator L defines a natural operation on L^p spaces: for f ∈ L^p(E,p,μ), L ∘ f ∈ L^p(F,p,μ).

Русский

Композиция с линейным оператором L, гладким по Lipshitza, задаёт естественную операцию на пространства L^p: если f ∈ L^p(E,p,μ), то L ∘ f ∈ L^p(F,p,μ).

LaTeX

$$$L: E \\to L_s[\\sigma] F$ и $f \\in L^p(E,p,\\mu)$ производят элемент $L \\circ f \\in L^p(F,p,\\mu)$; то есть операция композиции реализуется на пространствах $L^p$.$$

Lean4

/-- Composing `f : Lp` with `L : E →L[𝕜] F`. -/
def compLp (L : E →SL[σ] F) (f : Lp E p μ) : Lp F p μ :=
  L.lipschitz.compLp (map_zero L) f

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