English
Composition by a fixed continuous linear map L induces a bounded linear map on L^p spaces, Lp E p μ → Lp F p μ, given by f ↦ L ∘ f.
Русский
Композиция по фиксированному непрерывному линейному отображению L задаёт ограниченное линейное отображение на пространствах L^p: f ↦ L ∘ f.
LaTeX
$$$\\text{compLpL} : (L: E \\to SL[\\sigma] F) \\mapsto (f \\mapsto L \\circ f) \\in \\operatorname{Hom}_\\sigma(L^p(E,p,\\mu), L^p(F,p,\\mu)).$$$
Lean4
/-- Composing `f : Lp E p μ` with `L : E →L[𝕜] F`, seen as a `𝕜`-linear map on `Lp E p μ`. -/
def compLpₗ (L : E →SL[σ] F) : Lp E p μ →ₛₗ[σ] Lp F p μ
where
toFun f := L.compLp f
map_add' f
g := by
ext1
filter_upwards [Lp.coeFn_add f g, coeFn_compLp L (f + g), coeFn_compLp L f, coeFn_compLp L g,
Lp.coeFn_add (L.compLp f) (L.compLp g)]
intro a ha1 ha2 ha3 ha4 ha5
simp only [ha1, ha2, ha3, ha4, ha5, map_add, Pi.add_apply]
map_smul' c
f := by
ext1
filter_upwards [Lp.coeFn_smul c f, coeFn_compLp L (c • f), Lp.coeFn_smul (σ c) (L.compLp f), coeFn_compLp L f] with
_ ha1 ha2 ha3 ha4
simp only [ha1, ha2, ha3, ha4, Pi.smul_apply, map_smulₛₗ]
