norm_compContinuousMultilinearMap

English

The operator norm of the composed multilinear map is at most the product of the op-norms of the involved maps.

Русский

Норма оператора композиции много-линейного отображения не превосходит произведения норм оператора вовлечённых отображений.

LaTeX

$$$ \|g.mkContinuousLinear f C H\| ≤ \|g\| \cdot \prod_i \|f_i\| $$$

Lean4

theorem norm_compContinuousMultilinearMap (g : G →ₗᵢ[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
    ‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖ := by
  simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe, LinearIsometry.coe_toContinuousLinearMap,
    LinearIsometry.norm_map, ContinuousMultilinearMap.norm_def, Function.comp_apply]

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