English
A variant of the bound principle for the Schwartz space restricted to real line functions 𝓢(ℝ,F).
Русский
Вариант принципа ограничений для Schwartz-пространства, ограниченного функциями на ℝ: 𝓢(ℝ,F).
LaTeX
$$$\forall k,n, f\in 𝓢(\mathbb{R},F), M\in \mathbb{R}, M\ge 0, (\forall x\in \mathbb{R}, |x|^k \|\iteratedDeriv_n f(x)\| ≤ M) \Rightarrow \mathrm{seminorm}\,\mathbb{K}(k,n)(f) ≤ M$$$
Lean4
/-- If one controls the seminorm for every `x`, then one controls the seminorm.
Variant for functions `𝓢(ℝ, F)`. -/
theorem seminorm_le_bound' (k n : ℕ) (f : 𝓢(ℝ, F)) {M : ℝ} (hMp : 0 ≤ M)
(hM : ∀ x, |x| ^ k * ‖iteratedDeriv n f x‖ ≤ M) : SchwartzMap.seminorm 𝕜 k n f ≤ M :=
by
refine seminorm_le_bound 𝕜 k n f hMp ?_
simpa only [Real.norm_eq_abs, norm_iteratedFDeriv_eq_norm_iteratedDeriv]
