seminorm_le_bound — Mathlib

English

If a bound M controls all the weighted derivatives of f, then the corresponding seminorm is bounded by M.

Русский

Если существует неотрицательная константа M, контролирующая все взвешенные производные функции, то соответствующая семинормa не превосходит M.

LaTeX

$$$\forall k,n, f\in 𝓢(E,F), M\in \mathbb{R}, M\ge 0, (\forall x, \|x\|^k \|\ iteratedFDeriv_{\mathbb{R}}^n f(x)\| \le M) \Rightarrow \mathrm{seminorm}\,\mathbb{K}(k,n)(f) \le M$$$

Lean4

/-- If one controls the seminorm for every `x`, then one controls the seminorm. -/
theorem seminorm_le_bound (k n : ℕ) (f : 𝓢(E, F)) {M : ℝ} (hMp : 0 ≤ M)
    (hM : ∀ x, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ M) : SchwartzMap.seminorm 𝕜 k n f ≤ M :=
  f.seminormAux_le_bound k n hMp hM

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