nnnorm_changeOrigin_le — Mathlib

English

If the radius condition holds and x is given, the NN-norm of p.changeOrigin x k is bounded by a tsum involving p(k+l) and powers of ||x||.

Русский

При условии радиуса и заданного x НН-норма p.changeOrigin x k ограничена суммой по p(k+l) и степеням ||x||.

LaTeX

$$$\\|p.changeOrigin x k\\|_{+} \\le \\sum'_{l} \\|p(k+l)\\|_{+} \\cdot \\|x\\|_{+}^{l}$$$

Lean4

theorem nnnorm_changeOrigin_le (k : ℕ) (h : (‖x‖₊ : ℝ≥0∞) < p.radius) :
    ‖p.changeOrigin x k‖₊ ≤ ∑' s : Σ l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + s.1)‖₊ * ‖x‖₊ ^ s.1 :=
  by
  refine tsum_of_nnnorm_bounded ?_ fun l => p.nnnorm_changeOriginSeries_apply_le_tsum k l x
  have := p.changeOriginSeries_summable_aux₂ h k
  refine HasSum.sigma this.hasSum fun l => ?_
  exact ((NNReal.summable_sigma.1 this).1 l).hasSum

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