nnnorm_changeOriginSeriesTerm_apply_le

English

The NN-norm of changeOriginSeriesTerm is bounded by the product of norms: ‖p.changeOriginSeriesTerm k l s hs‖₊ ≤ ‖p(k+l)‖₊ · ‖x‖₊^l · ‖y‖₊^k.

Русский

Норма NN для changeOriginSeriesTerm ограничена произведением норм: ‖p.changeOriginSeriesTerm k l s hs‖₊ ≤ ‖p(k+l)‖₊ · ‖x‖₊^l · ‖y‖₊^k.

LaTeX

$$‖p.changeOriginSeriesTerm k l s hs (x)‖₊ ≤ ‖p(k+l)‧‖₊ · ‖x‖₊^l · ‖y‖₊^k$$

Lean4

theorem nnnorm_changeOriginSeriesTerm_apply_le (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) (x y : E) :
    ‖p.changeOriginSeriesTerm k l s hs (fun _ => x) fun _ => y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k :=
  by
  rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const]
  apply ContinuousMultilinearMap.le_of_opNNNorm_le
  apply ContinuousMultilinearMap.le_opNNNorm

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