norm_compContinuousLinearMap_le — Mathlib

English

The radius of p is bounded above by the radius of c•p, i.e., radius(p) ≤ radius(c•p).

Русский

Радиус p ограничен сверху радиусом c•p: radius(p) ≤ radius(c•p).

LaTeX

$$$p.radius \\le (c\\cdot p).radius.$$$

Lean4

theorem norm_compContinuousLinearMap_le (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) (n : ℕ) :
    ‖p.compContinuousLinearMap u n‖ ≤ ‖p n‖ * ‖u‖ ^ n :=
  by
  simp only [compContinuousLinearMap]
  apply le_trans (ContinuousMultilinearMap.norm_compContinuousLinearMap_le _ _)
  simp

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