norm_pow_mul_le_seminorm — Mathlib

English

A refined estimate expresses a bound involving the supremum of a finite set of seminorms over index pairs up to a bound m, with a factor depending on (1+||x||)^k.

Русский

Уточнённое неравенство связывает верхнюю границу через супремум по парам индексов до m и множитель (1+||x||)^k.

LaTeX

$$$(1+\|x\|)^k \|\iteratedFDeriv_{\mathbb{R}}^n f x\| \le 2^{m.1} \,(\mathrm{Iic}\; m).sup (\lambda m',\; \mathrm{seminorm}_{}\mathbb{K} m'.1 m'.2 (f))$$$

Lean4

theorem norm_pow_mul_le_seminorm (f : 𝓢(E, F)) (k : ℕ) (x₀ : E) : ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f :=
  by
  have := SchwartzMap.le_seminorm 𝕜 k 0 f x₀
  rwa [norm_iteratedFDeriv_zero] at this

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