le_seminormAux — Mathlib

English

For any Schwartz map f, every x satisfies the basic bound relating the n-th derivative to the seminormAux.

Русский

Для любого Schwartz-перехода f и точки x выполняется базовое неравенство, связывающее D^n f(x) и f.seminormAux.

LaTeX

$$$\\|x\\|^k \\cdot \\| \\mathrm{D}^n f(x) \\| \\le f.seminormAux_{k,n}$$$

Lean4

theorem le_seminormAux (k n : ℕ) (f : 𝓢(E, F)) (x : E) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ f.seminormAux k n :=
  le_csInf (bounds_nonempty k n f) fun _ ⟨_, h⟩ => h x

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