norm_iteratedFDeriv_le_seminorm — Mathlib

English

For any k and x0, the product of the k-th power of the norm of x0 and the value f at x0 is bounded by the k-seminorm of f.

Русский

Для любых k и точки x0 произведение ||x0||^k на значение f(x0) ограничено k-й семинормой SchwartzMap.

LaTeX

$$$\|x_0\|^k \|f(x_0)\| \le (\mathrm{seminorm}_{\mathbb{K}})(k,0)(f)$$$

Lean4

theorem norm_iteratedFDeriv_le_seminorm (f : 𝓢(E, F)) (n : ℕ) (x₀ : E) :
    ‖iteratedFDeriv ℝ n f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f :=
  by
  have := SchwartzMap.le_seminorm 𝕜 0 n f x₀
  rwa [pow_zero, one_mul] at this

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