nnnorm_changeOriginSeries_apply_le_tsum

English

For any k,l and point x, the NN-norm of p.changeOriginSeries k l applied to the constant vector x is bounded by the tsum of the NN-norms of p(k+l) multiplied by the l-th power of the NN-norm of x.

Русский

Для любых k,l и точки x НН-норма применения p.changeOriginSeries k l к константному вектору x не превышает суммарного значения, равного NN-норме p(k+l) умноженной на ||x||^l.

LaTeX

$$$\\|p.changeOriginSeries\\; k\\; l (\\cdot)\\|_{+} \\le \\sum'_{S: s.card = l} \\|p(k+l)\\|_{+} \\cdot \\|x\\|_{+}^{l}$$$

Lean4

theorem nnnorm_changeOriginSeries_apply_le_tsum (k l : ℕ) (x : E) :
    ‖p.changeOriginSeries k l fun _ => x‖₊ ≤
      ∑' _ : { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + l)‖₊ * ‖x‖₊ ^ l :=
  by
  rw [NNReal.tsum_mul_right, ← Fin.prod_const]
  exact (p.changeOriginSeries k l).le_of_opNNNorm_le (p.nnnorm_changeOriginSeries_le_tsum _ _) _

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