seminormAux — Mathlib

English

For each k, n, the seminormAux of a Schwartz map f is defined as the greatest lower bound of all nonnegative constants c that bound ∥x∥^k ∥D^n f(x)∥ for every x.

Русский

Для любых k, n семинормa f — это наименьшее неотрицательное число c, такое что для каждого x выполняется ∥x∥^k ∥D^n f(x)∥ ≤ c.

LaTeX

$$$\\mathrm{seminormAux}_{k,n}(f) = \\inf\\{ c \\in \\mathbb{R} \\mid 0 \\le c \\ \\wedge\\ \\forall x, \\|x\\|^k \\cdot \\| \\mathrm{D}^n f(x) \\| \\le c \\}$$$

Lean4

/-- Helper definition for the seminorms of the Schwartz space. -/
protected def seminormAux (k n : ℕ) (f : 𝓢(E, F)) : ℝ :=
  sInf {c | 0 ≤ c ∧ ∀ x, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ c}

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