smul_compLp — Mathlib

English

Scalar multiplication commutes with Lp-composition: (c • L) ∘ f = c • (L ∘ f) in L^p.

Русский

Умножение на скаляр и композиция на L^p коммутируют: (c·L) ∘ f = c·(L ∘ f) в L^p.

LaTeX

$$$ (c \\cdot L)\\circ f = c \\cdot (L\\circ f) \\quad \\text{in } L^p(μ).$$$

Lean4

theorem smul_compLp {𝕜''} [NormedRing 𝕜''] [Module 𝕜'' F] [IsBoundedSMul 𝕜'' F] [SMulCommClass 𝕜' 𝕜'' F] (c : 𝕜'')
    (L : E →SL[σ] F) (f : Lp E p μ) : (c • L).compLp f = c • L.compLp f :=
  by
  ext1
  grw [Lp.coeFn_smul, coeFn_compLp']
  refine (L.coeFn_compLp' f).mono fun x hx => ?_
  rw [Pi.smul_apply, hx, coe_smul', Pi.smul_def]

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