derivSeries_eq_zero — Mathlib

English

For any k, the NN-norm of p.changeOrigin x k is bounded by a tsum of products of p(k+l) with powers of ||x||.

Русский

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

LaTeX

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

Lean4

theorem derivSeries_eq_zero {n : ℕ} (hp : p (n + 1) = 0) : p.derivSeries n = 0 :=
  by
  suffices p.changeOriginSeries 1 n = 0 by ext v; simp [derivSeries, this]
  apply Finset.sum_eq_zero (fun s hs ↦ ?_)
  ext v
  have : p (1 + n) = 0 := p.congr_zero (by abel) hp
  simp [changeOriginSeriesTerm, ContinuousMultilinearMap.zero_apply, this]

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