isBoundedLinearMap_continuousMultilinearMap_comp_linear

English

Given a fixed linear map g, the map sending a bounded multilinear f to the multilinear map f( g m1, ..., g mn ) is bounded.

Русский

Пусть задано линейное отображение g; отображение f ↦ f(g m1, ..., g mn) определяет ограниченное линейное отображение по отношению к f.

LaTeX

$$$IsBoundedLinearMap\ 𝕜 \; (f: ContinuousMultilinearMap 𝕜 (⋯)\; F \to \text{G}) \rightarrow (f \mapsto f.compContinuousLinearMap (\lambda _\mapsto g))$$$

Lean4

/-- Given a fixed continuous linear map `g`, associating to a continuous multilinear map `f` the
continuous multilinear map `f (g m₁, ..., g mₙ)` is a bounded linear operation. -/
theorem isBoundedLinearMap_continuousMultilinearMap_comp_linear (g : G →L[𝕜] E) :
    IsBoundedLinearMap 𝕜 fun f : ContinuousMultilinearMap 𝕜 (fun _ : ι => E) F =>
      f.compContinuousLinearMap fun _ => g :=
  (ContinuousMultilinearMap.compContinuousLinearMapL (ι := ι) (G := F) (fun _ ↦ g)) |>.isBoundedLinearMap

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