le_seminorm — Mathlib

English

For any k, n, x, the weighted norm of the iterated derivative is bounded by the corresponding seminorm.

Русский

Для любых k, n, x взвешанная норма итеративной производной не превосходит соответствующей семинормы.

LaTeX

$$$\|x\|^k \|\iteratedFDeriv_{\mathbb{R}}^n f x\| \le \mathrm{seminorm}_{\mathbb{K}}(k,n)(f)$$$

Lean4

/-- The seminorm controls the Schwartz estimate for any fixed `x`. -/
theorem le_seminorm (k n : ℕ) (f : 𝓢(E, F)) (x : E) :
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ SchwartzMap.seminorm 𝕜 k n f :=
  f.le_seminormAux k n x

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