norm_compContinuousMultilinearMap_le

English

For a multilinear map f, there is a bound on the operator norm of mkContinuousMultilinear f C H in terms of C and the norms of the domain factors.

Русский

Для много-линейного отображения f существует ограничение на норму оператора mkContinuousMultilinear f C H в зависимости от C и норм компонент-области.

LaTeX

$$$ \|mkContinuousMultilinear f C H\| \le \max\{C,0\}$$$

Lean4

theorem norm_compContinuousMultilinearMap_le (g : G →L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
    ‖g.compContinuousMultilinearMap f‖ ≤ ‖g‖ * ‖f‖ :=
  ContinuousMultilinearMap.opNorm_le_bound (by positivity) fun m ↦
    calc
      ‖g (f m)‖ ≤ ‖g‖ * (‖f‖ * ∏ i, ‖m i‖) := g.le_opNorm_of_le <| f.le_opNorm _
      _ = _ := (mul_assoc _ _ _).symm

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