le_seminorm' — Mathlib

English

The operator norm of the iterated derivative at a point is bounded by the corresponding seminorm with k=0.

Русский

Норма операторной производной итерации в точке ограничена соответствующей семинормой при k=0.

LaTeX

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

Lean4

/-- The seminorm controls the Schwartz estimate for any fixed `x`.

Variant for functions `𝓢(ℝ, F)`. -/
theorem le_seminorm' (k n : ℕ) (f : 𝓢(ℝ, F)) (x : ℝ) : |x| ^ k * ‖iteratedDeriv n f x‖ ≤ SchwartzMap.seminorm 𝕜 k n f :=
  by
  have := le_seminorm 𝕜 k n f x
  rwa [← Real.norm_eq_abs, ← norm_iteratedFDeriv_eq_norm_iteratedDeriv]

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